@@ -205,3 +205,76 @@ COMPLETENESS_THEOREM
205205###Finite model property and decidability
206206
207207###Automated theorem proving and countermodel construction
208+
209+ ####In K
210+
211+ Our tactic` K_TAC ` and its associated rule` K_RULE ` can automatically prove theorems in the modal logic K.
212+
213+ Examples:
214+ ```
215+ K_RULE `!a b. [{} . {} |~ Box (a && b) <-> Box a && Box b]`;;
216+
217+ K_RULE `!a b. [{} . {} |~ Box a || Box b --> Box (a || b)]`;;
218+ ```
219+
220+ ####In GL
221+
222+ Our tactic` GL_TAC ` and its associated rule` GL_RULE ` can automatically prove theorems in the modal logic GL.
223+ Here is a list of examples
224+
225+ ####Example of a formula valid in GL but not in K
226+ ```
227+ time GL_RULE
228+ `!a. [GL_AX . {} |~ Box Diam Box Diam a <-> Box Diam a]`;;
229+ ```
230+
231+ ####Formalised Second Incompleteness Theorem
232+ In PA, the following is provable: If PA is consistent, it cannot prove its own consistency.
233+ ```
234+ let GL_second_incompleteness_theorem = GL_RULE
235+ `[GL_AX . {} |~ Not (Box False) --> Not (Box (Diam True))]`;;
236+ ```
237+
238+ ####PA ignores unprovability statements
239+ ```
240+ let GL_PA_ignorance = time GL_RULE
241+ `!p. [GL_AX . {} |~ (Box False) <-> Box (Diam p)]`;;
242+ ```
243+
244+ ####PA undecidability of consistency
245+ If PA does not prove its inconsistency, then its consistency is undecidable.
246+ ```
247+ let GL_PA_undecidability_of_consistency = time GL_RULE
248+ `[GL_AX . {} |~ Not (Box (Box False))
249+ --> Not (Box (Not (Box False))) &&
250+ Not (Box (Not (Not (Box False))))]`;;
251+ ```
252+ ####Undecidability of Godels formula
253+ ```
254+ let GL_undecidability_of_Godels_formula = time GL_RULE
255+ `!p. [GL_AX . {} |~ Box (p <-> Not (Box p)) && Not (Box (Box False))
256+ --> Not (Box p) && Not (Box (Not p))]`;;
257+ ```
258+
259+ ####Reflection and iterated consistency
260+ If a reflection principle implies the second iterated consistency assertion, then the converse implication holds too.
261+ ```
262+ let GL_reflection_and_iterated_consistency = time GL_RULE
263+ `!p. [GL_AX . {} |~ Box ((Box p --> p) --> Diam (Diam True))
264+ --> (Diam (Diam True) --> (Box p --> p))]`;;
265+ ```
266+
267+ ####A Godel sentence is equiconsistent with a consistency statement
268+ ```
269+ let GL_Godel_sentence_equiconsistent_consistency = time GL_RULE
270+ `!p. [GL_AX . {} |~ Box (p <-> Not (Box p)) <->
271+ Box (p <-> Not (Box False))]`;;
272+ ```
273+
274+ ####Arithmetical fixpoint
275+ For any arithmetical senteces p q, p is equivalent to unprovability of q --> p iff p is equivalent to consistency of q.
276+ ```
277+ let GL_arithmetical_fixpoint = time GL_RULE
278+ `!p q. [GL_AX . {} |~ Dotbox (p <-> Not (Box (q --> p))) <->
279+ Dotbox (p <-> Diam q)]`;;
280+ ```