Merge pull request #8 from Janis-Bai/coq-8.20

Add relevant parts of mechanisation of Bailitis' Bachelor's thesis

Author: JoJoDeveloping

README.md

@@ -9,12 +9,13 @@ The FOL library currently extends this core with the following content:
 - [Deduction](theories/Deduction): More deduction systems not included in the core library.
 - [Semantics](theories/Semantics): More semantics not included in the core library.
 - [Completeness](theories/Completeness): Completeness results for Tarski, Kripke, and algebraic semantics, constructive where possible.
-- [Incompleteness](theories/Incompleteness): An abstract and synthetic version of the first incompleteness theorem, instantiated to Robinson's Q.
+- [Incompleteness](theories/Incompleteness): An abstract and synthetic version of the first incompleteness theorem, instantiated to Robinson's Q, as well as a proof of the first incompleteness theorem and Tarski's theorem via Carnap's diagonal lemma.
 - [Tennenbaum](theories/Tennenbaum): Tennenbaum's theorem stating that the natural numbers are the only computable model of PA, constructivised.
 - [ArithmeticalHierachy](theories/ArithmeticalHierarchy): Semantic and syntactic characterisations of the arithmetical hierarchy and an equivalence proof.
 - [Proofmode](theories/Proofmode): A tool easing derivations in a deduction system, including a HOAS input language hiding de Bruijn encoded syntax.
 - [Reification](theories/Reification): A tactic automating representability proofs of Coq predicates as first-order formulas.
 - [Utils](theories/Utils): A collection of additional results needed in various projects.
+- [HilbertSystem](theories/HilbertSystem): A Hilbert system for first-order logic with a proof of its equivalence to natural deduction.
 
 ## Installation
 

theories/HilbertSystem/hilbert_system.v

@@ -0,0 +1,46 @@
+From Undecidability.FOL Require Import Syntax.Core Arithmetics.Robinson.
+From FOL Require Import ProofMode.
+Require Import List.
+
+Section Hil_def.
+    Context {Σ_funcs : funcs_signature}.
+    Context {Σ_preds : preds_signature}.
+    Existing Instance falsity_on. 
+
+    (** * Hilbert Systems *)
+
+    Implicit Type p : peirce.
+
+    Inductive hilAx: forall (ff: falsity_flag) (p: peirce), form -> Prop :=
+    | HK phi psi {p}: hilAx p (phi → psi → phi)
+    | HS phi psi tau {p}: hilAx p ((phi → psi → tau) → (phi → psi) → phi → tau)
+    | CI phi psi {p}: hilAx p (phi → psi → phi ∧ psi)
+    | CE1 phi psi {p}: hilAx p (phi ∧ psi → phi)
+    | CE2 phi psi {p}: hilAx p (phi ∧ psi → psi)
+    | DI1 phi psi {p}: hilAx p (phi → phi ∨ psi)
+    | DI2 phi psi {p}: hilAx p (psi → phi ∨ psi)
+    | DE phi psi tau {p}: hilAx p (phi ∨ psi → (phi → tau) → (psi → tau) → tau)
+    | Ebot phi {p}: hilAx p (⊥ → phi)
+    | AllE t phi {p}: hilAx p ((∀ phi) → phi[t..])
+    | AllG phi {p}: hilAx p (phi → ∀ phi[↑])
+    | AllD phi psi {p}: hilAx p ((∀ phi → psi) → (∀ phi) → (∀ psi)) 
+    | ExI phi t {p}: hilAx p (phi[t..] → ∃ phi)
+    | ExE phi psi {p}: hilAx p ((∃ phi) → (∀ phi → psi[↑]) → psi)
+    | PC phi psi: hilAx class (((phi → psi) → phi) → phi).
+
+    Inductive hilprv A |: forall (p: peirce), form -> Prop :=
+    | MP phi psi {p}: hilprv p phi -> hilprv p (phi → psi) -> hilprv p psi
+    | HilAx phi n {p}: hilAx p phi -> hilprv p (forall_times n phi)
+    | ThAx phi {p}: In phi A -> hilprv p phi.
+
+    Definition thilprv {p: peirce} (T: form -> Prop) (phi: form):=
+        exists A, (forall phi, In phi A -> T phi) /\ hilprv A p phi.
+
+End Hil_def.
+
+Notation "A ⊢H phi" := (hilprv A _ phi) (at level 55).
+Notation "A ⊢HI phi" := (@hilprv _ _ A intu phi) (at level 55).
+Notation "A ⊢HC phi" := (@hilprv _ _ A class phi) (at level 55).
+Notation "T ⊢HT phi" := (thilprv T phi) (at level 55).
+Notation "T ⊢HTI phi" := (@thilprv _ _ intu T phi) (at level 55).
+Notation "T ⊢HTC phi" := (@thilprv _ _ class T phi) (at level 55).