I want to prove that Peano axioms are consistent with coq and defined them so
Axiom nt : Type.
Axiom znt : nt.
Axiom snt : nt -> nt.
Definition nt_neq := forall n: nt, znt <> snt n.
Definition nt_inv := forall n: nt, n = znt / exists n', n = snt n'.
Definition nt_inj := forall n m: nt, snt n = snt m -> n = m.
Definition nt_ind := forall P : nt -> Prop,
P znt ->
(forall n : nt, P n -> P (snt n)) ->
forall n : nt, P n.
want to prove their irrefutability
Theorem nt_irr : ~~(nt_neq / nt_inv / nt_inj / nt_ind).
We can in fact instantiate and prove these axioms.
Definition nt := nat.
Definition znt := Z.
Definition snt := S.
(* Define nt_neq etc. *)
Theorem nt_irr : nt_neq / nt_inv / nt_inj / nt_ind.
Proof.
(* exercise for the reader *)
Qed.
There is some confusion in your terminology. The “irrefutability of the Peano axioms” is better stated by putting the double negation on the outside of the quantification on the nt
type and its primitives. Then it’s a straightforward consequence of the fact that the axioms are provable.
Record Peano_theory : Type :=
{ nt : Type
; znt : nt
; snt : nt
; nt_NEQ : forall n: nt, znt <> snt n
; (* other axioms here *)
}.
Theorem Peano_theory_provable : Peano_theory.
Proof.
refine {| nt := nat ; znt := Z ; snt := S |}.
(* exercise for the reader *)
Qed.
(* inhabited : Type -> Prop
https://coq.inria.fr/doc/V8.20.0/stdlib/Coq.Init.Logic.html#inhabited *)
Theorem Peano_theory_irrefutable : ~~ inhabited Peano_theory.
Proof.
intros H; apply H; constructor; apply Peano_theory_provable.
Qed.
Irrefutability (in the sense of double negation) is not the same thing as consistency. A proof of irrefutability (~~Axioms
) implies that you can’t derive a contradiction (consistency) only if you also assume that Coq—or whatever logical system the proof of ~~Axioms
lives in—is consistent in the first place. And you can’t say anything about the converse. A set of Axioms
could be consistent with Coq without there being a proof of irrefutability, ~~Axioms
. Consistency is really a meta-theoretical property, meaning that it’s a property about the logical system (Coq here), which cannot be stated or proved inside of that system. To propertly state consistency as a formal property, one would need to model the logical system explicitly, which entails the many subtleties difficulties of formalizing a logical system within a logical system.
2