Proof in predicate calculus

  • Thread starter solakis
  • Start date
  • #1
19
0

Main Question or Discussion Point

Let:

1)P be one place operation

2)K be one place operation

3) c be a constant


let :

1) G be a two place predicate

2) H be a two place predicate

Let :

The following axioms or assumptions)

1)for all A { H(A,c)v H(c,A)v G(A,c)}

2)for all A { H(A,c)=> G[P(A),A]}

3)for all A {H(c,A) => G[P(A),K(A)]}

4)for all A {G[K(A),c] => G(A,c)}.

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),c] => G(A,c)}
 

Answers and Replies

  • #2
CompuChip
Science Advisor
Homework Helper
4,302
47
Sounds like an interesting exercise, I'll try it later.
Have you finished it yet, or are you just fishing around for the answer? :-)
 
  • #3
CompuChip
Science Advisor
Homework Helper
4,302
47
Just got home from work and had a serious look at the problem.
It's an interesting problem.
I found the way to do it, but I haven't written down the complete formal proof because I don't really feel like proving OR elimination for three variables at this point (i.e. { A v B v C, A => D, B => D, C => D } |= D).
 

Related Threads on Proof in predicate calculus

  • Last Post
Replies
1
Views
2K
  • Last Post
Replies
7
Views
2K
  • Last Post
Replies
9
Views
2K
  • Last Post
Replies
2
Views
1K
Replies
10
Views
5K
  • Last Post
Replies
7
Views
2K
  • Last Post
Replies
4
Views
2K
Replies
3
Views
2K
  • Last Post
Replies
23
Views
3K
  • Last Post
Replies
0
Views
3K
Top