1
$\begingroup$

Consider a certain formal system with only axiom Excluded Middle -$EM$

enter image description here

and 18 inference rules:

9 implicative ruules (clearly not independent)

enter image description here

and 9 tautological rules:

enter image description here

If we have substitution at hands as well but we are restricted no to use conditional proof.

Is this particular system complete?

I always believed that the system is complete. But once I decided to prove or disprove completeness I stuck. I neither can find any reference neither nor can proof completeness.

If someone is familiar with this system I would be grateful to have some reference or proof.

Improve this question
$\endgroup$
7
  • $\begingroup$ Where does the system come from? $\endgroup$
    – Emil Jeřábek
    Commented Jun 1, 2020 at 12:54
  • $\begingroup$ This is a system we usually offer to students in first common logic course for students of non-mathematical profile, in order they understand what is concept of proof. $\endgroup$
    – Evgeny Kuznetsov
    Commented Jun 1, 2020 at 13:53
  • 2
    $\begingroup$ What exactly do you mean by “tautological rules”? I assumed, as the notation suggests, that these are just inference rules that can be applied in both directions (on whole lines in the proof). However, do you by any chance mean that they can be actually applied as replacement rules anywhere deep inside the formulas? If the latter, then the calculus is easily seen to be complete. $\endgroup$
    – Emil Jeřábek
    Commented Jun 1, 2020 at 15:37
  • $\begingroup$ @Emil Jeřábek Yes, you see it correctly, tautological rules work both direction. How do we see completeness of the calculus? $\endgroup$
    – Evgeny Kuznetsov
    Commented Jun 5, 2020 at 13:09
  • $\begingroup$ That does not answer what I asked. Can the tautological rules be applied only to whole formulas, or also to subformulas? $\endgroup$
    – Emil Jeřábek
    Commented Jun 5, 2020 at 13:10

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .