Require Import Undecidability.FOL.Util.Syntax.
Require Import Undecidability.FOL.Util.FullTarski.
Require Import Undecidability.FOL.Util.FullDeduction.
Import Vector.VectorNotations.
Require Import List.
Existing Instance falsity_on.
Inductive PA_funcs : Type :=
Zero : PA_funcs
| Succ : PA_funcs
| Plus : PA_funcs
| Mult : PA_funcs.
Definition PA_funcs_ar (f : PA_funcs ) :=
match f with
| Zero => 0
| Succ => 1
| Plus => 2
| Mult => 2
end.
Inductive PA_preds : Type :=
Eq : PA_preds.
Definition PA_preds_ar (P : PA_preds) :=
match P with
| Eq => 2
end.
Instance PA_funcs_signature : funcs_signature :=
{| syms := PA_funcs ; ar_syms := PA_funcs_ar |}.
Instance PA_preds_signature : preds_signature :=
{| preds := PA_preds ; ar_preds := PA_preds_ar |}.
Declare Scope PA_Notation.
Open Scope PA_Notation.
Notation "'zero'" := (@func PA_funcs_signature Zero ([])) (at level 1) : PA_Notation.
Notation "'σ' x" := (@func PA_funcs_signature Succ ([x])) (at level 32) : PA_Notation.
Notation "x '⊕' y" := (@func PA_funcs_signature Plus ([x ; y]) ) (at level 39) : PA_Notation.
Notation "x '⊗' y" := (@func PA_funcs_signature Mult ([x ; y]) ) (at level 38) : PA_Notation.
Notation "x '==' y" := (@atom PA_funcs_signature PA_preds_signature _ _ Eq ([x ; y])) (at level 40) : PA_Notation.
Notation "x '⧀' y" := (∃ (x[↑] ⊕ σ $0) == y) (at level 42) : PA_Notation.
Definition ax_zero_succ := ∀ (zero == σ var 0 ~> falsity).
Definition ax_succ_inj := ∀∀ (σ $1 == σ $0 ~> $1 == $0).
Definition ax_add_zero := ∀ (zero ⊕ $0 == $0).
Definition ax_add_rec := ∀∀ ((σ $0) ⊕ $1 == σ ($0 ⊕ $1)).
Definition ax_mult_zero := ∀ (zero ⊗ $0 == zero).
Definition ax_mult_rec := ∀∀ (σ $1 ⊗ $0 == $0 ⊕ $1 ⊗ $0).
Definition ax_induction (phi : form) :=
phi[zero..] ~> (∀ phi ~> phi[σ $0 .: S >> var]) ~> ∀ phi.
Definition FA := ax_add_zero :: ax_add_rec :: ax_mult_zero :: ax_mult_rec :: nil.
Definition ax_cases := ∀ $0 == zero ∨ ∃ $1 == σ $0.
Definition Q := FA ++ (ax_zero_succ::ax_succ_inj::ax_cases::nil).
Inductive PA : form -> Prop :=
PA_FA phi : In phi FA -> PA phi
| PA_discr : PA ax_zero_succ
| PA_inj : PA ax_succ_inj
| PA_induction phi : PA (ax_induction phi).
Definition ax_refl := ∀ $0 == $0.
Definition ax_sym := ∀∀ $1 == $0 ~> $0 == $1.
Definition ax_trans := ∀∀∀ $2 == $1 ~> $1 == $0 ~> $2 == $0.
Definition ax_succ_congr := ∀∀ $0 == $1 ~> σ $0 == σ $1.
Definition ax_add_congr := ∀∀∀∀ $0 == $1 ~> $2 == $3 ~> $0 ⊕ $2 == $1 ⊕ $3.
Definition ax_mult_congr := ∀∀∀∀ $0 == $1 ~> $2 == $3 ~> $0 ⊗ $2 == $1 ⊗ $3.
Definition EQ :=
ax_refl :: ax_sym :: ax_trans :: ax_succ_congr :: ax_add_congr :: ax_mult_congr :: nil.
Definition FAeq :=
EQ ++ FA.
Definition Qeq :=
EQ ++ Q.
Inductive PAeq : form -> Prop :=
PAeq_FA phi : In phi FAeq -> PAeq phi
| PAeq_discr : PAeq ax_zero_succ
| PAeq_inj : PAeq ax_succ_inj
| PAeq_induction phi : PAeq (ax_induction phi).
Notation extensional M :=
(forall x y, @i_atom _ _ _ M Eq ([x ; y]) <-> x = y).
Definition entailment_FA phi :=
valid_ctx FAeq phi.
Definition deduction_FA phi :=
FAeq ⊢I phi.
Definition entailment_Q phi :=
valid_ctx Qeq phi.
Definition deduction_Q phi :=
Qeq ⊢I phi.
Definition entailment_PA phi :=
forall D (I : interp D) rho, (forall psi rho, PAeq psi -> rho ⊨ psi) -> rho ⊨ phi.
Definition ext_entailment_PA phi :=
forall D (I : interp D) rho, extensional I -> (forall psi rho, PA psi -> rho ⊨ psi) -> rho ⊨ phi.
Definition deduction_PA phi :=
PAeq ⊢TI phi.