0
$\begingroup$

I'm having trouble understanding the question below.

The question

A Hilbert proof system is based on the axioms

  1. $\alpha \to (\beta \to \alpha)$
  2. $( \alpha \to ( \beta \to \gamma ) ) \to ( ( \alpha \to \beta ) \to ( \alpha \to \gamma ) )$
  3. $( \lnot \beta \to \lnot \alpha ) \to ( ( \lnot \beta \to \alpha ) \to \beta )$

and the Modus Ponens inference rule. Which of the axioms above (or none) can be proved with the Suppes inference system?

My issue

The course handout claims that by definition

  1. A sentence $\phi$ can be inferred with the Suppes system from a set of premises $\Sigma$, denoted $\Sigma\vdash_S \phi$, if and only if there exists a Suppes-proof $\alpha_1, \ldots, \alpha_n$, so that $\alpha_n = \phi$ and the suppositional assumption or hypothesis $H_n = \emptyset$.
  2. A sentence is a theorem in a Suppes system, if and only if $\emptyset \vdash_S \phi$

What I'm asking is, is the question referring to the first or the second part of the definition above? My guess is the second part, but I'm not sure. Second, what is the definition actually saying? Should I be able to construct a Suppes proof (a Fitch diagram/table) without any premises (how is this supposed to be done?) to show that the axioms are theorems, or do I need to come up with premises that would lead to the conclusion?

Also, what is the difference between an assumption and a premise?

The Suppes system

The Suppes system of inference consists of the following main inference rules.

  • Modus Ponens (MP): $$ \frac{ \alpha \to \beta \qquad \alpha }{ \beta } $$

  • Modus Tollendo Tollens (TT): $$\frac{ \alpha \to \beta \qquad \lnot \beta}{ \lnot \alpha }$$

  • Modus Tollendo Ponens (TP): $$\frac{ \alpha \lor \beta \qquad \lnot \alpha }{ \beta }$$

  • Exchange rules (CE) and (DE): $$\frac{ \alpha \land \beta }{ \beta \land \alpha } \quad\text{and}\quad \frac{ \alpha \lor \beta }{ \beta \lor \alpha }$$

  • Then there's the usual rules for conditional and indirect proofs (CP) and (IP): $$\frac{ \substack{[\alpha] \\ \vdots \\ \beta} }{ \alpha \to \beta } \quad\text{and}\quad \frac{ \lnot \beta \to \alpha \land \lnot \alpha }{ \beta }$$.

Also a myriad of inclusion and elimination rules exists, but this exposition is already taking enough space in my opinion.

$\endgroup$
9
  • 2
    $\begingroup$ Yes, you have to prove $\emptyset \vdash_S (\alpha \to (\beta \to \alpha))$ and so on. $\endgroup$ – Mauro ALLEGRANZA Mar 5 '20 at 13:48
  • 1
    $\begingroup$ @MauroALLEGRANZA Alright. But how do I start with no premises? Can I choose anything that I want, or are there restrictions? Surelu I need to make some assumptions to be able to prove anything? $\endgroup$ – SeSodesa Mar 5 '20 at 13:49
  • 2
    $\begingroup$ The issue is: do you know Suppes' proof system ? $\endgroup$ – Mauro ALLEGRANZA Mar 5 '20 at 13:51
  • $\begingroup$ Not very well. I have a list of the different inference rules, but based on the question, I'm not sure if I'm allowed to use all of them or not. The lecture notes could also be clearer/less abstract. $\endgroup$ – SeSodesa Mar 5 '20 at 13:58
  • 2
    $\begingroup$ NO: (CP). 1) assume $[\alpha]$; 2) assume $[\beta]$; 3) derive $\alpha$ from 1); 4) $\beta \to \alpha$ from 2) by (CP); 5) $\alpha \to (\beta \to \alpha)$ from 1) by (CP). $\endgroup$ – Mauro ALLEGRANZA Mar 5 '20 at 14:51
1
$\begingroup$

Hint

Consider the 2nd axiom (a little bit less trivial than the firs one):

1) $a \to (b \to c)$ --- assumed [A]

2) $a \to b$ --- assumed [B]

3) $a$ --- assumed [C]

4) $b$ --- from 3) and 4) by MP

5) $b \to c$ --- from 1) and 3) by MP

6) $c$ --- from 4) and 5) by MP

$a \to c$ --- from 3) and 6) by CP, discharging assumption [C]

The result follow by two more applications of CP.


The proof of the 3rd axiom needs MP, conjunction introduction, CP and IP.

$\endgroup$
1
  • $\begingroup$ Thank you. You helped a lot, but I also had to dig up an old handout from a few years back. Its not that this is mathematically difficult, but I needed more explicit examples to really jostle my memory on how formal proofs are supposed to be written. $\endgroup$ – SeSodesa Mar 5 '20 at 17:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.