MHB T: Is the Proof in Predicate Calculus Correct?

  • Thread starter Thread starter solakis1
  • Start date Start date
  • Tags Tags
    Calculus Proof
solakis1
Messages
407
Reaction score
0
Let :
1)P one place operation
.........m is a constant......
2)K one place operation

let :
1) G two place predicate
2) H two place predicate
Let :
The following axioms or assumptions)
1)for all A { H(A,m)v H(m,A)v G(A,m)}
2)for all A { H(A,m)=> G[P(A),A]}
3)for all A {H(m,A) => G[P(A),K(A)]}
4)for all A {G[K(A),m] => G(A,m)}.
5)for all A,B,C { [G(A,B) and G(A,C)]=> G(B,C)}
Then formally prove :
for all A {G[P(A),m] => G(A,m)}
 
Physics news on Phys.org
This problem has two parts: proving the claim informally and then translating the proof into a formal derivation. The second part depends on the formal system, i.e., the definition of a derivation. I have not though about this problem, but have you proved this statement on paper?
 
Evgeny.Makarov said:
This problem has two parts: proving the claim informally and then translating the proof into a formal derivation. The second part depends on the formal system, i.e., the definition of a derivation. I have not though about this problem, but have you proved this statement on paper?

No

How do we prove the statement informaly??

Do we have informal proofs in predicate calculus?
 
start with axiom (1) (that looks the most promising). we can assume G(P(A),m).

if G(A,m) there's nothing to prove (note: it may "make more sense" to prove that if not H(A,m) and not H(m,A) then necessarily G(A,m), essentially "saving this case for last").

if H(A,m), then G(P(A),A) by (2), so we have G(A,m) by (3)

(since we have G(P(A),A) and G(P(A),m)).

if H(m,A), then we have G(A,m) by (3) and (4) and transitivity of implication.

i have no idea what i just proved, but I'm pretty sure i did it "informally".
 
Deveno said:
start with axiom (1) (that looks the most promising). we can assume G(P(A),m).

if G(A,m) there's nothing to prove (note: it may "make more sense" to prove that if not H(A,m) and not H(m,A) then necessarily G(A,m), essentially "saving this case for last").

if H(A,m), then G(P(A),A) by (2), so we have G(A,m) by (3)

(since we have G(P(A),A) and G(P(A),m)).

if H(m,A), then we have G(A,m) by (3) and (4) and transitivity of implication.

i have no idea what i just proved, but I'm pretty sure i did it "informally".

I wonder could that informal proof be checked thru a computer program??
 
solakis said:
I wonder could that informal proof be checked thru a computer program??

An informal proof is for the benefit of Humans who want to understand what is going on. An informal proof must be translated into a formal proof for machine verification (or translated from a formal to informal proof for the benefit of Humans if the proof is in fact machine generated).

CB
 
solakis said:
I wonder could that informal proof be checked thru a computer program??
I indeed formalized this proof in Coq. Here is the script.

Code:
Parameters (T : Type) (m : T) (p k : T -> T) (G H : T -> T -> Prop).

Axiom a1 : forall A,  H A m \/ H m A \/ G A m.
Axiom a2 : forall A,  H A m-> G (p A) A.
Axiom a3 : forall A, H m A -> G (p A) (k A).
Axiom a4 : forall A, G (k A) m -> G A m.
Axiom a5 : forall A B C, G A B -> G A C-> G B C.

Theorem t : forall A, G (p A) m -> G A m.
Proof.
intros A P. (* assume A and P : G (p A) m *)
destruct (a1 A) as [? | [? | ?]].
(* Case when H A m *)
+ assert (G (p A) A) by (apply a2; trivial).
  eapply a5; eauto.
(* Case when H m A *)
+ assert (G (p A) (k A)) by (apply a3; trivial).
  assert (G (k A) m) by (eapply a5; eauto).
  apply a4; trivial.
(* Case when G A m *)
+ trivial.
Qed.

In fact, Coq is smart enough to prove most of the claim automatically:

Code:
Theorem t1 : forall A, G (p A) m -> G A m.
Proof.
intros; destruct (a1 A) as [? | [? | ?]]; eauto.
Qed.

Note that this is not a formal derivation; this is a script consisting of commands that generate a derivation. The derivation of t1 is

Code:
t1 = 
fun (A : T) (H0 : G (p A) m) =>
let o := a1 A in
match o with
| or_introl H1 => a5 (p A) A m (a2 A H1) H0
| or_intror (or_introl H2) => a4 A (a5 (p A) (k A) m (a3 A H2) H0)
| or_intror (or_intror H2) => H2
end

I don't expect anyone here to understand this, but if you want to try, disjunction is right-associative in Coq, so or_introl H1 is the case when H1 : H A m, or_intror (or_introl H2) is when H2 : H m A and or_intror (or_intror H2) is when H2 : G A m.

As I said in another thread, this derivation is also isomorphic to a derivation in natural deduction, so it can be straightforwardly translated, for example, into Fitch notation.
 
CaptainBlack said:
An informal proof is for the benefit of Humans who want to understand what is going on. An informal proof must be translated into a formal proof for machine verification (or translated from a formal to informal proof for the benefit of Humans if the proof is in fact machine generated).

CB

Why,do you understand the informal proof Deveno wrote??
 
Last edited:
solakis said:
Why,do you understand the informal proof Deveno wrote??

That would require that I were interested enough in the original question to read the question and purported proof in detail. But I'm not, mainly because formal logics are of no intrinsic interest to me.

CB
 
Back
Top