A proof in the Hilbert-style axiom system

Click For Summary
SUMMARY

The discussion focuses on constructing a formal proof for the statement ## \vdash ((A \rightarrow B) \rightarrow C) \rightarrow (B \rightarrow C)## using a Hilbert-style axiom system. The proof must utilize modus ponens and four specific axioms: A1, A2, A3, and A4. The approach involves strategically modifying initial statements and applying modus ponens to derive the desired conclusion. The final proof successfully demonstrates the required logical implication without relying on the deduction theorem.

PREREQUISITES
  • Understanding of Hilbert-style axiom systems
  • Familiarity with modus ponens
  • Knowledge of sentential logic axioms A1, A2, A3, and A4
  • Basic skills in constructing formal proofs
NEXT STEPS
  • Study the application of modus ponens in formal proofs
  • Learn more about Hilbert-style axiom systems and their properties
  • Explore the deduction theorem and its implications in logic
  • Practice constructing proofs using various sentential logic axioms
USEFUL FOR

Students of logic, particularly those new to formal proof construction, as well as educators seeking to guide learners through the intricacies of sentential logic and Hilbert-style systems.

PWiz
Messages
695
Reaction score
117

Homework Statement


Provide a complete formal proof that ## \vdash ((A \rightarrow B) \rightarrow C)
\rightarrow (B \rightarrow C)##.

Homework Equations


I am only allowed to use modus ponens and these four 'sentential logic' axioms:
A1 ## \neg \alpha \rightarrow (\alpha \rightarrow \beta)##
A2 ##\beta \rightarrow (\alpha \rightarrow \beta)##
A3 ##(\alpha \rightarrow \beta) \rightarrow ((\neg \alpha \rightarrow \beta) \rightarrow \beta)##
A4 ##(\alpha \rightarrow (\beta \rightarrow \gamma )) \rightarrow ((\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \gamma ))##

The Attempt at a Solution


I have no idea where to begin. I'm thinking about using axiom 2, but I don't know how I would proceed from there. The problem would become easy if I was allowed to 'add an antecedent', but I am not allowed to directly do that. Any help is appreciated. Please note that I am a new student to logic, and I have only studied zero-order logic until now, so kindly provide hints that I will be able to understand. (The homework is due tomorrow!)
 
Physics news on Phys.org
These kind of proofs are much easier if you have the deduction theorem. What the deduction theorem says is that:

If you can prove Y using X as an axiom, then you can prove X \rightarrow Y​

You don't have the deduction theorem, but you can use it as a strategy for finding the proof, as follows:

A proof of S is a sequence of statements S_1, S_2, ..., S_n such that each statement is either an axiom, or follows from two previous statements by modus ponens, and such that the last statement is S. So:
  1. See if you can construct a proof of C where the first statement is (A \rightarrow B) \rightarrow C and the second statement is B. So this original proof will have C as its last sentence.
  2. Now, modify your proof as follows: Starting with the third statement, replace each statement S by the modified statement B \rightarrow S. Now, see if you can add additional steps so that you prove each modified statement without using B as an axiom. After these modifications, you will have a proof where B \rightarrow C is the last statement.
  3. Now, modify your proof again: Starting with the new third statement, replace each statement S by the modified statement ((A \rightarrow B) \rightarrow C) \rightarrow S. Now, see if you can add additional steps so that you can prove each modified statement without using (A \rightarrow B) \rightarrow C as an axiom. After these modifications, you will have a proof where ((A \rightarrow B) \rightarrow C) \rightarrow (B \rightarrow C) is the last statement.
  4. Now, get rid of the first two statements, since you are no longer using them. Now you have a proof of ((A \rightarrow B) \rightarrow C) \rightarrow (B \rightarrow C)
 
  • Like
Likes   Reactions: PWiz and Greg Bernhardt
Thanks, I got it!
 

Similar threads

  • · Replies 4 ·
Replies
4
Views
3K
  • · Replies 6 ·
Replies
6
Views
5K
  • · Replies 5 ·
Replies
5
Views
2K
  • · Replies 10 ·
Replies
10
Views
1K
  • · Replies 2 ·
Replies
2
Views
3K
  • · Replies 2 ·
Replies
2
Views
3K
  • · Replies 43 ·
2
Replies
43
Views
5K
Replies
2
Views
2K
  • · Replies 4 ·
Replies
4
Views
784
  • · Replies 5 ·
Replies
5
Views
2K