Welcome to our community

Be a part of something great, join today!

proof in predicate calculus 2

solakis

Active member
Dec 9, 2012
304
Let:

1) m be a constant

2) P ,K be one place operation symbols

3) F be two places operation symbol


4) H,G be two places predicate symbols



Let, the following assumptions:


1) $\forall A\forall B [ H(A,m)\Longrightarrow G[P(A),B]\Longleftrightarrow G[K(B),A]\wedge H(B,m)]$


2) $\forall A\forall B[ H(A,m)\wedge H(B,m)\Longrightarrow H(F(A,B),m)]$

3)$\forall A\forall B\forall C\forall D[ G[A,B]\wedge G[C,D]\Longrightarrow G[F(A,C),F(B,D)]]$

4)$\forall A\forall B [ G[F(K(P(A)),K(P(B))),K(F(P(A),P(B)))]]$

5)$\forall A\forall B\forall C [ G[A,B]\wedge G[A,C]\Longrightarrow G[B,C]]$

6) $\forall A [ G(A,A) ]$

Then prove :

$\forall A\forall B [ H(A,m)\wedge H(B,m)\Longrightarrow G[ P(F(A,B)),F(P(A),P(B))]]$
 

Evgeny.Makarov

Well-known member
MHB Math Scholar
Jan 30, 2012
2,492
In premise (1), is it

H(A,m) => (G[P(A),B] <=> G[K(B),A] /\ H(B,m))

or

(H(A,m) => G[P(A),B]) <=> G[K(B),A] /\ H(B,m)?

Also, this is a metamathematical question, but why is this problem interesting? Without knowing the semantics of P, K, F, H and G, it's just some manipulation of symbols. I am not sure how it gives any additional insight into logic.
 

solakis

Active member
Dec 9, 2012
304
In premise (1), is it

H(A,m) => (G[P(A),B] <=> G[K(B),A] /\ H(B,m))

or

(H(A,m) => G[P(A),B]) <=> G[K(B),A] /\ H(B,m)?

Also, this is a metamathematical question, but why is this problem interesting? Without knowing the semantics of P, K, F, H and G, it's just some manipulation of symbols. I am not sure how it gives any additional insight into logic.

It is : H(A,m) => (G[P(A),B] <=> G[K(B),A] /\ H(B,m))

Well is it not every mathematical proof a manipulation of symbols??
 

CaptainBlack

Well-known member
Jan 26, 2012
890
It is : H(A,m) => (G[P(A),B] <=> G[K(B),A] /\ H(B,m))

Well is it not every mathematical proof a manipulation of symbols??
Actually no, this is a fiction foisted on us by certain philosophies of mathematics.

A proof is an argument that convinces mathematicians. What counts as proof changes with time and context.

CB
 

solakis

Active member
Dec 9, 2012
304

CaptainBlack

Well-known member
Jan 26, 2012
890
How is anyone convinced of anything. Look at Euclid, it is full of "proofs" that were considered convincing for over 2000 years.

CB
 

solakis

Active member
Dec 9, 2012
304
How is anyone convinced of anything.
Not of anything ,but of a mathematical argument.

Anyway that is what i asked you



Look at Euclid, it is full of "proofs" that were considered convincing for over 2000 years.

CB
Euclid along with his "elements " wrote a book called "Pseudaria".

The contents and the magnitude of its validity can be found in Proclus,p.70,1- 18

The book is considered to be the 1st proof checker in human history (at least for the Geometrical theorems,that is).

Unfortunately the book was irreparably lost.