1

I have given a correct and complete calculus for propositional logic:

$$(A1)~\psi\rightarrow(\varphi\rightarrow\psi)\\ (A2)~(\psi\rightarrow(\varphi\rightarrow\chi))\rightarrow((\psi\rightarrow\varphi)\rightarrow(\psi\rightarrow\chi))\\ (A3)~(\lnot\varphi\rightarrow\lnot\psi)\rightarrow(\psi\rightarrow\varphi)\\ (R1)~\text{If }\vdash\psi\text{ and }\vdash\psi\rightarrow\varphi\text{, then }\vdash\varphi.$$

In order to prove something (the deduction theorem), I need the general formulation of the modus ponens, i.e.

$(R1')~\text{If }\Gamma\vdash\psi\text{ and }\Gamma\vdash\psi\rightarrow\varphi\text{, then }\Gamma\vdash\varphi.$

Can I somehow prove $(R1')$ or do I have to take it as another axiom?

So far, I have mentioned that $\Gamma\vdash\psi$ means that $\psi$ holds if all $\varphi\in\Gamma$ hold. If all formulas of a superset of $\Gamma$ hold then especially all $\varphi\in\Gamma$ hold, therefore $\Gamma\vdash\psi$ implies $\Gamma\cup X\vdash\psi$ for all $X\subseteq\textit{PL}$. (monotonicity of $\vdash$)

Even though $(R1')$ basically states $\left(\big(\bigwedge\Gamma\Rightarrow\psi\big)\land\big(\bigwedge\Gamma\Rightarrow\psi\rightarrow\varphi\big)\right)\Rightarrow\big(\bigwedge\Gamma\Rightarrow\varphi\big)$, which is equivalent to $\bigwedge\Gamma\Rightarrow\left(\big(\psi\land(\psi\rightarrow\varphi)\big)\Rightarrow\varphi\right)$, and I can show $\Gamma\vdash(\psi\land(\psi\rightarrow\varphi))\rightarrow\varphi$ by using monoticity of $\vdash$, since $\vdash(\psi\land(\psi\rightarrow\varphi))\rightarrow\varphi$ holds, I would need the deduction theorem to be proven already in order for this to be helpful. Is there another way? I am free to use the semantics of propositional logic as an argument, as the calculus is correct and complete.

JMP
  • 21,771
xamid
  • 258
  • For the sake of the problem Im sure you can take modus ponens as a given. Its not an axiom; it can be proven from simpler statements. – CogitoErgoCogitoSum Mar 21 '17 at 01:45
  • 1
    And I want to know how can it be proven. – xamid Mar 21 '17 at 08:54
  • I think that first you need the notion of "derivation from assumption" : $\Gamma \vdash \varphi$. – Mauro ALLEGRANZA Mar 22 '17 at 13:25
  • But in this case you have to state the MP rule without the "restriction" : $\vdash$. With it standing, you can only prove tautologies, and the fact that you can add (by monotonicity) unused premises $\Gamma$ does not change the fact that in this way the $\varphi$ in $\Gamma \vdash \varphi$ is a tautology, simply because you must have first a derivation $\vdash \varphi$ and after you add the premises. – Mauro ALLEGRANZA Mar 22 '17 at 13:27
  • @MauroALLEGRANZA Yes, that's exactly what I have been trying to tell the OP as well. I believe the OP is confused about what $R1$ means. Could you please take a look at my Answer? Thanks! – Bram28 Mar 23 '17 at 13:27
  • @MauroALLEGRANZA You are right. So I had to argue for the validity of $(R1')$ by definition of the semantics, since it holds for semantic consequence, and mention that the deduction theorem holds for propositional logic using powerful enough rules of inference. But my calculus does not define derivation powerful enough to use its proofs to prove the DT. – xamid Mar 24 '17 at 11:43
  • Ok, but we are in a loop... You are right in sayingthat the DT is a (meta-)theorem, i.e. it must be proved in the meta-theory and it is not part of the calculus, while axioms and rules of inference a part of the calculus. But in its simpler form, DT says : "if we have a derivation of $\beta$ from assumption $\alpha$, we have also (and we have a "receipe" to build it) a derivation of $\alpha \to \beta$. – Mauro ALLEGRANZA Mar 24 '17 at 12:10
  • The last is: $\vdash \alpha \to \beta$ but the first is: $\alpha \vdash \beta$. Thus - and this is the gist of my comments and the repeated comments by @Bram28 - you need the "syntactical" definition of derivation from assumption: $\Gamma \vdash \varphi$. Without this def, you simply cannot prove (meta-tehoretically) nothing about it, because if you do not define it, it does not exist in your "logical machinery". – Mauro ALLEGRANZA Mar 24 '17 at 12:12
  • In conclusion, you need two things: (i) the def of derivation from assumptions: $\Gamma \vdash \varphi$ and (ii) a "more liberal" def of modus ponens : "from $\psi$ and $\psi \to \varphi$, derive $\varphi$", removing the "restriction": $\vdash$. – Mauro ALLEGRANZA Mar 24 '17 at 12:15
  • @MauroALLEGRANZA Agreed. $\vdash$ is typically used as a meta-logical symbol, but in this case they use it to define an inference rule (which should be frowned upon, I agree!), just as Metamath does: http://us.metamath.org/mpegif/mmset.html#axioms. Mauro, have you seen that use of defining inference rules using $\vdash$ elsewhere? I actually had never seen that before. The explanation they provide on that website for why they use the $\vdash$ is kind of interesting as well ... – Bram28 Mar 24 '17 at 12:38
  • @Bram28 - interesting ! (metamath) It seems to me that its source (in part) is W&R's Principia and I suppose that the source of misundestanding about the use of $\vdash$ is exactly the muddled explanation of modus ponens in Principia (but they do not formulate it with $\vdash$ !). – Mauro ALLEGRANZA Mar 24 '17 at 13:04
  • In "mature" math log textbook, starting from 1928 Hilbert and Ackermann, following through Kleene (1952) and Church (1956), the correct rule is stated: "from the two formulas $\mathfrak A$ and $\mathfrak A \to \mathfrak B$, the new formula $\mathfrak B$ is obtained." – Mauro ALLEGRANZA Mar 24 '17 at 13:07
  • @Bram28 - Frege (1879) formulated mp as "From the two judgements $\vdash B \to A$ and $\vdash B$, the new judgment $\vdash A$ follows." But the "judgement stroke" $\vdash$ for Frege does not stay for "it is a theorem" but for "it is an assertion (judgement)" and thus it is compatible with an assumption (also if Frege as well as W&R Principia have no concept of "derivation from assumptions"). – Mauro ALLEGRANZA Mar 24 '17 at 13:26
  • I think it's not a loop, it is only that my calculus does not define syntactic derivation but rather makes only statements about it. – xamid Mar 24 '17 at 13:46
  • @MauroALLEGRANZA Interesting, thanks!! – Bram28 Mar 24 '17 at 16:48
  • @xamid But then that's not much of a calculus then ... it would merely be a collection of meta-logical statements about some otherwise undefined calculus. – Bram28 Mar 24 '17 at 16:49
  • @MauroALLEGRANZA A professor supervising my thesis about logics agreed with me that I can define syntactic consequence $\Gamma\vdash\psi$ using my axiom schemata and $(R1')$, while then giving Łukasiewicz's calculus which only provides statements without assumptions ($\emptyset\vdash\psi~=:~\vdash\psi$) and does not define $\vdash$ itself. It is of interest that this weak calculus is sufficient for completeness and what the deduction theorem tells us about the connection of both approaches. – xamid Mar 24 '17 at 16:54

2 Answers2

2

I believe you are (understandably!) not interpreting the $R1$ rule correctly:

$(R1)~\text{If }\vdash\psi\text{ and }\vdash\psi\rightarrow\varphi\text{, then }\vdash\varphi.$

Since the $\vdash$ is typically used as a meta-logical theorem to express the derivability of some statement from other statements through the use of inference rules of some proof system (or calculus, as you call it), you understandably interpret this rule indeed as a kind of meta-theorem regarding the derivability of statements: "If $\psi$ is derivable (without any assumptions), and $\psi \rightarrow \varphi$ is derivable (without any assumptions), then $\varphi$ is derivable (without any assumptions)"

However, I am fairly sure the intended interpretation of $R1$ in the book (I don't have access to the book, so I can't tell for sure) is not as a meta-logical theorem, but as an inference rule. In fact, it would be your very Modus Ponens:

"If you are doing a derivation, and at some point you have $\psi$ as well as $\psi \rightarrow \varphi$ as lines in your derivation, then you can write down $\varphi$ as a line in your derivation"

In our discussions, you seem to indicate that $A1,A2, and A3$ are to be treated as statements about derivability such as well, i.e. that they can be written as:

$(A1)\vdash ~\psi\rightarrow(\varphi\rightarrow\psi)\\ (A2)\vdash ~(\psi\rightarrow(\varphi\rightarrow\chi))\rightarrow((\psi\rightarrow\varphi)\rightarrow(\psi\rightarrow\chi))\\ (A3)\vdash ~(\lnot\varphi\rightarrow\lnot\psi)\rightarrow(\psi\rightarrow\varphi)$

and where, as such, they are again to be seen as meta-logical theorems: "any statement of the form $\psi\rightarrow(\varphi\rightarrow\psi)$ is derivable"

Interestingly, this is exactly how Metamath (http://us.metamath.org/mpegif/mmset.html#axioms) describes its axioms.

But again, I believe $A1$, $A2$, and $A3$ should be seen as inference rules, which simply say (in the case of A1): "At any point during a derivation you can write down a line of the form $\psi\rightarrow(\varphi\rightarrow\psi)$"

Indeed, I think a purist would frown upon Metamath's use of $\vdash$ to define its inference rules, since inference rules are just that: inference rules. While meta-logical statements (for which we would use $\vdash$) are statements about the power of some set of inference rules.

I have several reasons for believing that, while R1 used the meta-logical symbol $\vdash$, it is really just used to define the Modus Ponens inference rule:

  • Any axiomatic system that I have seen has Modus Ponens as a given inference rule, and $R1$ seems to fit that bill reading it the way I do. Indeed, while Metamath describes $A1,A2,A3,R1$ using the $\vdash$, it does not treat $A1,A2,A3,R1$ as meta-logical theorems, but as inference rules.
  • If $R1$ is not an inference rule (and possibly $A1,A2,A3$ aren't either), then how are you supposed to perform any actual inferences?
  • Indeed, if $R1$ (and possibly $A1,A2,A3$) are meta-logical theorems about the derivability of statements, then what proof system is it a meta-logical theorem of? What is it talking about?!

In the discussion you say that $\Gamma \vdash \varphi$ iff $\Gamma \vDash \varphi$, but we have to make that statement $\Gamma \vdash \varphi$ relative to specific proof systems. Indeed, it is easy to come up with proof systems where this does not hold. That is, you can have proof systems that are not sound and complete. For example, take a proof system (call it $N$, for 'Null') that has no inference rules at all. That system is (trivially) sound, but hopelessly incomplete. So, we don't have $\Gamma \vdash_N \varphi$ iff $\Gamma \vDash \varphi$. Or take a proof system (call it $Q$) that has the 'Hokus Ponens' rule that says that at any point during a derivation you can put down any statement you want. $Q$ is (trivially) complete, but hopelessly unsound. So, again, we don't have $\Gamma \vdash_Q \varphi$ iff $\Gamma \vDash \varphi$.

So, when you seem to indicate that you want to prove some kind of derivability ($\vdash$) claim on the basis of a logical consequence claim $\vDash$), you are putting the cart before the horse! First you need to define what $\vdash$ means for a particular system $S$, and then you can try to prove $\Gamma \vdash_S \varphi$ iff $\Gamma \vDash \varphi$

Indeed, the very use of $\vdash$ without indexing it to specify what proof system we are talking about is circumspect. Even worse, when you make claims like "it does not matter how we define it, because we have $\Gamma \vdash \varphi$ iff $\Gamma \vDash \varphi$", I am getting really concerned. Yes, we sometimes say that for propositional logic (and first-order logic) $\Gamma \vdash \varphi$ iff $\Gamma \vDash \varphi$, and as such we say that 'propositional logic is complete' and 'first-order logic is complete', but we do that because there exist proof systems for which this is true, and typically we use exactly such systems. But given any particular system $S$, we cannot simply assume that $\Gamma \vdash_S \varphi$ iff $\Gamma \vDash \varphi$: we would actually need to prove that (and, given the earlier examples of systems $N$ and $Q$, this may simply not be the case).

In other words, if $R1$ is supposed to be a derivability statement, as you take it to be, then you have to specify what proof system we are talking about, i.e. $R1$ would need to be formulated as:

$(R1)~\text{If }\vdash_S \psi\text{ and }\vdash_S\psi\rightarrow\varphi\text{, then }\vdash_S\varphi.$

where $S$ is a specific proof system. But this is not how $R1$ is described. Why not? You know my answer: Because I think it is really just an inference rule, not a meta-logical theorem.

Now, your $R1'$ is a meta-logical theorem though. And to be sure, let's specify that the proof system consisting of $A1,A2,A3,R1$ is system $HS$ (for Hilbert system), so we can properly write down $R1'$:

$(R1')~\text{If }\Gamma \vdash_{HS} \psi\text{ and }\Gamma \vdash_{HS}\psi\rightarrow\varphi\text{, then }\Gamma \vdash_{HS}\varphi.$

But $R1'$ follows immediately from the fact that $HS$ contains $R1$:

Suppose $\Gamma \vdash_{HS} \varphi$ and $\Gamma \vdash_{HS} \varphi \rightarrow \psi$

To show that $\Gamma \vdash_{HS} \psi$ do the following:

Start with $\Gamma$ as your premises.

Since $\Gamma \vdash_{HS} \varphi$, we now we can derive $\varphi$

Similarly, since $\Gamma \vdash_{HS} \varphi \rightarrow \psi$, we can also derive $\varphi \rightarrow \psi$

And now apply R1 on $\varphi$ and $\varphi \rightarrow \psi$ to get $\psi$

So, starting with $\Gamma$, we can derive $\psi$. And so $\Gamma \vdash_{HS} \psi$

Finally, please note that as a meta-logical theorem, R1' is not an inference rule, and it is not your typical Modus Ponens, which is an inference rule. An inference rule is part of a proof system (or calculus as you call it) that lets us derive statements from other statements. A meta-logical theorem is a claim about what such proof systems can or cannot derive. Indeed, if R1 itself is taken as a meta-logical theorem (as you seem to take it), then for this system it would not even be true that $\vdash P \rightarrow P$, even if $A1$, $A2$, and $A3$ are to be taken as axioms or inference rules that lets you derive statements of the respective forms, because you have no further inference rule to actually combine those statements to derive other statements (like $P \rightarrow P$).

Bram28
  • 100,612
  • 6
  • 70
  • 118
  • 1
    But my $(R1)$ works only if $\vdash\varphi$ and $\vdash\varphi\rightarrow\psi$ hold (i.e. they are tautologies), which is not the case. You want to use $(R1')$ which I want to prove. – xamid Mar 21 '17 at 08:51
  • @xamid Oh, I see what you mean. Well, then you have a problem, since then A1, A2, A3, and R1 can only derive tautologies. – Bram28 Mar 21 '17 at 13:44
  • Can you prove that? In the above comments @CogitoErgoCogitoSum stated that it could be proven from simpler statements, but he did neither prove his claim, and your statements are contradicting each other. I would be surprised if there is no valid argumentation for $(R1')$ based on $(R1)$, since they are similar. – xamid Mar 22 '17 at 11:36
  • @xamid Yes. The statement you can get by the application of A1, A2, and A3 are tautologies. And the way you interpret R1, which is: if you can derive $\varphi$ from nothing, and if you can derive $\varphi \rightarrow \psi$ from nothing, then you can derive $\psi$. Now, since the only statements you can get from nothing are the ones you can get through A1, A2, and A3, which are all tautologies, that means that any statements of the form $\varphi$ and $\varphi \rightarrow \psi$ that you can get from nothing are tautologies as well ... and that means that $\psi$ has to be a tautology as well. – Bram28 Mar 22 '17 at 11:39
  • I dont understand what you mean. I want to show $(R1')$. You say you can show even based on the above explaination of syntactic consequence $(\vdash)$, you could prove this impossible. How? Also note that we are talking about metatheorems. (To your edit: This shows only that you cannot derive it only from $(A1),(A3),(R1)$, but it doesn't consider the definition of syntactic consequence $\Gamma\vdash\psi$ for $\Gamma\ne\emptyset$.) – xamid Mar 22 '17 at 11:44
  • @xamid I just showed how you can only derive tautologies from nothing using these rules. Now, you could start with other statements (non-tautologies) as your premises, but the way you interpret R1, you can't use those to infer other statements from, since you say that R1 can only derive $\psi$ from $\varphi \rightarrow \psi$ and $\varphi$ if those latter two are derived from nothing, i.e. not using given premises. So, you still can't infer any non-tautologies using the rules. But since R1' rule can derive non-tautologies, you can't derive the R1' from the others. – Bram28 Mar 22 '17 at 11:49
  • @xamid I just explained how the case $\Gamma \not = \emptyset$ doesn't help you. Again, the way you interpret R1, you can't use those statements from $\Gamma$ to infer other statements from using R1, and obviously you don't use them with A1, A2, and A3 either. – Bram28 Mar 22 '17 at 11:51
  • Of course, you cannot state something like $\Gamma\vdash\psi$ when you didn't define what it means. That's why I defined that in my original post. Since we are talking about metatheorems, however, we can use much more than only $(A1)$-$(A3),(R1)$. A metatheorem is stated in a metatheory, which is all of mathematics (i.e. second-order logics, set theory, etc.). – xamid Mar 22 '17 at 11:52
  • @xamid I don't understand your talk about 'metatheorems': $\vdash$ is purely about what you can syntactically infer from what, i.e. What statements you can infer from what statements using the given rules. And I just explained why, given the rules A1, A2, and A3, and the way you interpret R1, you cannot derive new non-tautologies, e.g. You cannot derive $Q$ given $P$ and $P \rightarrow Q$. But note my emphasis on your interpretation of R1 ... I believe that you misread R1, and that R1 really is just Modus Ponens as it is normally defined. Where did you get these rules? From lecture? A book? – Bram28 Mar 22 '17 at 11:57
  • $(R1)$ does not define syntactic consequence of the calculus (It is not stated ${\psi,\psi\rightarrow\varphi}\vdash\varphi$ !!), it is a metatheorem (rule of inference). In the system, I know that the deduction theorem holds. I just cannot prove it, since I don't know how to argue for $(R1')$, which holds there, too. There has to be an argumentation for these valid metatheorems, i.e. a proof (or our metasystem is incomplete, which then has to be shown). Such a proof is what I am asking for. – xamid Mar 22 '17 at 12:01
  • I got these rules from a book, isbn 9783884050675. – xamid Mar 22 '17 at 12:05
  • @xamid Ok, I'll try to look it up. One more quick comment though: At the start of your post you say that the 4 given rules form a complete proof system. I can already tell you that that is only true in 2 cases: Case 1) we never provide any given $\Gamma$, and the system is designed to merely prove tautologies from nothing. In that case, you are never going to get your R1', as I explained in earlier comments. Case 2) The system can work with given $\Gamma$ ... But then the system is complete only when R1 is interpreted as the general Modus Ponens rules, i.e. your R1' . My bet is the latter. – Bram28 Mar 22 '17 at 12:14
  • I didn't misread it, such rules of inference are a very common thing. The provided system by the way originates from Jan Łukasiewicz, it is his $L_3$ system, as listed here: http://projecteuclid.org/download/pdf_1/euclid.pja/1195522378 It is even sometimes necessary so state rules like that. Here is a paper noting the apparent misunderstanding about rules of inferences that you seem to have: http://link.springer.com/article/10.1007%2Fs11229-011-9905-9 – xamid Mar 22 '17 at 12:20
  • @xamid I tried looking up the book ... it is some German book? Anyway, I don't have access to it, and without that I can't tell you for certain how R1 is supposed to be used. I do know that most accounts of proof systems of the type you describe in your post have a bunch of axioms (like A1,A2, and A# .. and these 3 axioms are indeed commonly used), and in addiction to that they have Modus Ponens as a given inference rule. This is why I suspect that your R1 is meant as Modus Ponens as well. – Bram28 Mar 22 '17 at 14:49
  • The same system is for example also used by Metamath (see Section 3.3.1.: http://us.metamath.org/downloads/metamath.pdf), and it is also stated in my first link from my previous comment. www.metamath.org has a huge framework of proofs that show you exactly how $(R1)$ is used. – xamid Mar 22 '17 at 17:12
  • @xamid Yes, I am familiar with metamath. They indeed have exactly the rules you indicate in your post. And so the rule your book calls R1 they call Modus Ponens. And how do they use Modus Ponens? They use it completely consistent with my original answer: they allow for you to start with a set of statements $\Gamma$ (they are called Hypotheses in metamath), and then using the axioms and Modus Ponens you can derive other things. So now you can indeed prove things other than logical tautologies, and indeed rule R1' can be derived from R1 exactly as I did in my original answer. – Bram28 Mar 22 '17 at 17:51
  • Apparently, you didn't understand the basics of propositional logic. They do not use $\Gamma\ne\emptyset$ for $\Gamma\vdash\psi$ ever. They only use rules of the form ${\vdash\psi_1,\dots,\vdash\psi_n} \ {\Rightarrow}\ \vdash\varphi$ (i.e. rules of inference). Note that $\vdash\psi$ means $\emptyset\vdash\psi$. They use a 'rule of modus ponens' which is also only a rule of inference. – xamid Mar 22 '17 at 18:56
  • @xamid In metamath, and every other axiomatic system that I have seen, they use the Modus Ponens rule as follows: If you are in the middle of doing a derivation, and you have a statement $\varphi$, as well as a statement $\varphi \rightarrow \psi$, then you can write down a new statement $\psi$ by reference to those two earlier statements. So it works as an inference rule, and it is exactly what I did in my original answer to prove your R1', which I took to be a meta-logical theorem (like the Deduction theorem). – Bram28 Mar 22 '17 at 19:02
  • @xamid Also, the Modus Ponens rule in Metamath does not require $\varphi$ and $\varphi \rightarrow \psi$ to be tautologies. For example, they use axioms for set theory, which are not logical tautologies, but they are happy to derive theorems from that using Modus Ponens. – Bram28 Mar 22 '17 at 19:05
  • Again, you are wrong. Metamath requires for the 'rule of modus ponens' (stated at http://us.metamath.org/downloads/metamath.pdf Section 3.3.1, page 64) that both, $\varphi$ and $\varphi\rightarrow\psi$ are tautologies, which is denoted by $\vdash\varphi$ and $\vdash\varphi\rightarrow\psi$. They have more axioms for set theory, which I do not refer to. Apparently then you didn't understand a single axiomatic system with a rule of modus ponens. Again, http://link.springer.com/article/10.1007%2Fs11229-011-9905-9 refers to this common mistake. NOTE: – xamid Mar 22 '17 at 19:23
  • A rule of inference only states that the derivability of some formulas $\alpha_1,\dots,\alpha_n$ implies the derivability of a formula $\beta$. It does not state, that $\beta$ would be derivable from $\alpha_1,\dots,\alpha_n$. – xamid Mar 22 '17 at 19:23
  • @xamid So if a rule of inference doesn't derive any statements from other statements, are there any rules that do derive statements from other statements? – Bram28 Mar 22 '17 at 19:50
  • Not in the propositional calculus. But as stated, we are talking about metatheorems, so that doesn't matter. We need to argue for $(R1')$, based on a definition for syntactic consequence (which is also part of our metasystem). – xamid Mar 22 '17 at 20:02
  • @xamid But if a rule of inference only states that the derivability of some formulas $\alpha_1,…,\alpha_n$ implies the derivability of a formula $\beta$, then every rule of inference (at least for propositional logic) would be true, right? Because the antecedent would always be false. Because nothing is actually derivable (for propositional logic). – Bram28 Mar 22 '17 at 20:11
  • A calculus makes some 'derivability statements' (but does not define the syntactic consequence relation itself) with rules of inference stating what is derivable, and correct and complete calculi show that all tautologies are derivable from $\emptyset$, by definition of the calculi. Syntactic consequence has to be defined according to semantic consequence, i.e. such that $\Gamma\vDash\psi$ iff $\Gamma\vdash\psi$. So the semantics of propositional logic is required for arguments here. – xamid Mar 22 '17 at 20:23
  • @xamid OK, but does this particular calculus you have at the beginning of your post have the ability to actually infer anything? Because if not, then it is not true that $\Gamma \vDash \psi$ iff $\Gamma \vdash \psi$. – Bram28 Mar 22 '17 at 20:37
  • Once again, the calculus itself infers deductions, but it does not deduct itself. $\Gamma\vDash\psi$ iff $\Gamma\vdash\psi$ is a statement in our metasystem. We use the calculus to infer deductions that are consequences by definition of the consequence relation. A semantic consequence for propositional logic is defined such that $\Phi\vDash\psi$ iff for all interpretations $\mathfrak{I}$ that are models of all $\varphi\in\Phi$, $\mathfrak{I}$ is also a model of $\psi$. – xamid Mar 22 '17 at 20:53
  • @xamid Thank you for your definition of $\vDash$! So how do you define $\vdash$? – Bram28 Mar 22 '17 at 20:56
  • I don't know. It doesn't matter, since $\Gamma\vDash\psi$ iff $\Gamma\vdash\psi$, as propositional logic is consistent and complete. – xamid Mar 22 '17 at 20:57
  • P.s. should the $\vdash$ be included in the definition of A1, A2, and A3? e.g. A1: $\vdash \psi \rightarrow (\varphi \rightarrow \psi)$? That's how they have it on metamath. – Bram28 Mar 22 '17 at 20:58
  • @xamid What do you mean by propositional logic is consistent and complete? Aren't consistency and completeness statements about proof systems for propositional logic? That is, wouldn't a proof system that includes the inference rule "Hokus Ponens: from nothing infer $\phi$" be inconsistent? – Bram28 Mar 22 '17 at 20:59
  • I didn't explicitly state that $\vdash\psi$ holds for every axiom, i.e. every formula instantiable from $(A1),(A2),(A3)$. But that's what those axiom schemata mean, indeed. – xamid Mar 22 '17 at 21:01
  • I stated propositional logic to be consistent and complete. A theory is consistent (in semantical terms) if and only if it has a model, i.e., there exists an interpretation under which all formulas in the theory are true. It is complete, if there exists a formal system with syntactic derivation $\vdash$ such that $\vDash\psi\ {\Rightarrow}\ \vdash\psi$, i.e. every tautology can be derived in a finite amount of steps. – xamid Mar 22 '17 at 21:11
  • @xamid OK, so the $\vdash$ is understood to be relative to a proof system, right? So for example, if I have a proof system (call it $S$) that has Hokus Ponens as an inference rule, then for that proof system it holds that ${ P } \vdash Q$. Or better put: ${ P } \vdash_S Q$. Agreed? – Bram28 Mar 22 '17 at 21:33
  • MP as inference rule is still ${\vdash\psi,\vdash\psi\rightarrow\varphi}\ {\Rightarrow}\ \vdash\varphi$ while MP as deduction would be ${\psi,\psi\rightarrow\varphi}\vdash\varphi$. Ok, I guess I have to simply prove MP as deduction over semantic consequence.. which includes to construct a finite deduction for it in every case. – xamid Mar 22 '17 at 21:43
  • Thanks for your edited answer, but I still think you are wrong (also I have linked you a paper that also states that, two times), and the correct way is to argue using semantics (which I also did now, in my thesis). Are you a PhD or a professor in formal sciences, or where did you get your understanding about logics? I am writing my thesis in logics in theoretical computer science, and to make sure I am right, I will talk today to one of my two supervising professors who are both logicians. – xamid Mar 24 '17 at 10:52
  • My professor agreed with me in my understanding of rule $(R1)$, and generally in the metatheoretical character of rules of inference (and by the way everything that contains $\vdash$). He however also mentioned that rules such as $(R1)$ without any assumptions are rather ancient. We concluded also that I can define syntactic consequence $\Gamma\vdash\psi$ using my axiom schemata and $(R1')$, while then giving Łukasiewicz's calculus which only provides statements without assumptions ($\emptyset\vdash\psi~=:~\vdash\psi$), and does not define $\vdash$ itself. – xamid Mar 24 '17 at 16:47
  • @xamid. Right, if you treat R1 as a meta-logical rule, then you can't get R1' from that, since you can only get tautologies using R1. So you would indeed have to assert R1' ... or change R1 into R1'. – Bram28 Mar 24 '17 at 16:55
0

It turned out that in order to talk about conditional syntactic consequence $\Gamma\vdash\psi$, we need to define $\vdash$ based on sequences of formulas that are proofs, and use a derivation rule of modus ponens $\{\psi,\psi\rightarrow\varphi\}\vdash\varphi$ which is based on the semantic consequence, especially on $\{\psi,\psi\rightarrow\varphi\}\vDash\varphi$.

  1. Define the semantics:

    The semantics of PL is given by a function $⟦\cdot⟧^\mathfrak{I}:\textit{PL}\rightarrow\{0,1\}$, such that ${\forall \psi,\varphi:}$

    • $⟦\lnot\psi⟧^\mathfrak{I}:=1-⟦\psi⟧^\mathfrak{I}$
    • $⟦\psi\lor\varphi⟧^\mathfrak{I}:=\textit{max}\left\{⟦\psi⟧^\mathfrak{I},⟦\varphi⟧^\mathfrak{I}\right\}$
    • $⟦\psi⟧^\mathfrak{I}:=\mathfrak{I}(\psi)$, for variable $\psi\in\tau$ and an interpretation $\mathfrak{I}:\tau\rightarrow\{0,1\}$

    A formula $\psi\in\textit{PL}$ is valid, if $⟦\psi⟧^\mathfrak{I}\,{=}\,1$ holds for all interpretations $\mathfrak{I}$ of variables.

    Semantic consequence of PL is a relation $\vDash\,\subseteq2^\textit{PL}\times\textit{PL}$ with $\Gamma\vDash\psi$ iff for every interpretation $\mathfrak{I}$ with $\forall\varphi\in\Gamma:⟦\varphi⟧^\mathfrak{I}=1$ follows $⟦\psi⟧^\mathfrak{I}=1$.

  2. Show the foundation of modus ponens, i.e. $\{\psi,\psi\rightarrow\varphi\}\vDash\varphi$:

    Due to ${⟦\psi\rightarrow\varphi⟧^\mathfrak{I}}=⟦\lnot\psi\lor\varphi⟧^\mathfrak{I}=max\left\{⟦\lnot\psi⟧^\mathfrak{I},⟦\varphi⟧^\mathfrak{I}\right\}=max\left\{1-⟦\psi⟧^\mathfrak{I},⟦\varphi⟧^\mathfrak{I}\right\}\text{, therefore}$ $\begin{array}{@{}r@{}l@{}} {⟦\psi⟧^\mathfrak{I}=1\land⟦\psi\rightarrow\varphi⟧^\mathfrak{I}=1}~\Rightarrow&{⟦\psi⟧^\mathfrak{I}=1\land max\left\{1-⟦\psi⟧^\mathfrak{I},⟦\varphi⟧^\mathfrak{I}\right\}=1}\\ ~\Rightarrow&{⟦\psi⟧^\mathfrak{I}=1\land(1-⟦\psi⟧^\mathfrak{I}=1\lor⟦\varphi⟧^\mathfrak{I}=1)}\\ ~\Rightarrow&{⟦\psi⟧^\mathfrak{I}=1\land(⟦\psi⟧^\mathfrak{I}=0}\lor⟦\varphi⟧^\mathfrak{I}=1)\\ ~\Rightarrow&{({⟦\psi⟧^\mathfrak{I}=1\land⟦\psi⟧^\mathfrak{I}=0})\lor(⟦\psi⟧^\mathfrak{I}=1\land⟦\varphi⟧^\mathfrak{I}=1)}\\ ~\Rightarrow&⟦\varphi⟧^\mathfrak{I}=1, \end{array}$

    we have ${\{\psi,\psi\rightarrow\varphi\}\vDash\varphi}$, for all $\psi,\varphi\in\textit{PL}$.

  3. Define syntactic consequence:

    For ${\psi,\varphi\in\textit{PL}}$, we define the derivation of modus ponens as $\{\psi,\psi\rightarrow\varphi\}\vdash\varphi$. $(\textit{MP})$

    A proof under conditions $\Gamma\subseteq\textit{PL}$, denoted $\Gamma$-proof, for a formula $\varphi_n\in\textit{PL}$ is a finite sequence of formulas $\sigma=\varphi_1,\dots,\varphi_n$ such that for all ${i\in\{1,\dots,n\}}$ holds: $\begin{array}{@{}l@{}}\begin{array}{@{}r@{\,}c@{\,}l@{}}\varphi_i\in\Gamma & \cup & \left\{\psi\rightarrow(\varphi\rightarrow\psi)~\middle|~\psi,\varphi\in\textit{PL}\right\}\\ & \cup & \left\{(\psi\rightarrow(\varphi\rightarrow\chi))\rightarrow((\psi\rightarrow\varphi)\rightarrow(\psi\rightarrow\chi))~\middle|~\psi,\varphi,\chi\in\textit{PL}\right\}\\ & \cup & \left\{(\lnot\varphi\rightarrow\lnot\psi)\rightarrow(\psi\rightarrow\varphi)~\middle|~\psi,\varphi\in\textit{PL}\right\}\text{, or}\end{array}\\ \exists j,m:(j<m<i)\land\left(\{\varphi_j,\varphi_m\}\overset{(\textit{MP})}{\vdash}\varphi_i\right)\end{array}$

    We say $\psi$ is a syntactic consequence of $\Gamma$, denoted $\Gamma\vdash\psi$, if there is a $\Gamma$-proof for $\psi$. Typical connotations are $\vdash\psi$ for $\emptyset\vdash\psi$, $\varphi\vdash\psi$ for $\{\varphi\}\vdash\psi$, and $\Gamma,\varphi\vdash\psi$ for $\Gamma\cup\{\varphi\}\vdash\psi$.

Now that we have defined syntactic consequence, we can prove $(R1')$:

  1. (Theorem) It holds $\left\{\Gamma\vdash\psi,\Gamma\vdash\psi\rightarrow\varphi\right\}\Rightarrow\Gamma\vdash\varphi$, for ${\Gamma\subseteq\textit{PL}}$ and ${\psi,\varphi\in\textit{PL}}$. $(R1')$

    (Proof) By $\Gamma\vdash\psi$, there is a $\Gamma$-proof $\sigma_\psi=\psi_1,\dots,\psi_m$ with $\psi_m=\psi$, and by $\Gamma\vdash\psi\rightarrow\varphi$, there is a $\Gamma$-proof $\sigma_{\psi\rightarrow\varphi}=\psi_1',\dots,\psi_n'$ with $\psi_n'=\psi\rightarrow\varphi$. We can now construct a $\Gamma$-proof $\sigma_\varphi=\sigma_\psi,\sigma_{\psi\rightarrow\varphi},\varphi$, since $\{\psi_m,\psi_n'\}=\{\psi,\psi\rightarrow\varphi\}\overset{(\textit{MP})}{\vdash}\varphi$. $\square$

The calculus

$(A1)~\psi\rightarrow(\varphi\rightarrow\psi)\\ (A2)~(\psi\rightarrow(\varphi\rightarrow\chi))\rightarrow((\psi\rightarrow\varphi)\rightarrow(\psi\rightarrow\chi))\\ (A3)~(\lnot\varphi\rightarrow\lnot\psi)\rightarrow(\psi\rightarrow\varphi)\\ (R1)\left\{\vdash\psi,\vdash\psi\rightarrow\varphi\right\}\Rightarrow~\vdash\varphi$

now follows directly from the definition of syntactic consequence and $(R1')$:

$(R1)$ is the special case for $(R1')$ with $\Gamma=\emptyset$. It is important to note that the calculus $(A1),(A2),(A3),(R1)$ does not define syntactic consequence, but it is a system to infer statements about unconditional syntactic consequence (for which soundness and completeness can be shown).

It is now possible to prove the deduction theorem as desired, using $(MP)$ and/or $(R1')$.

xamid
  • 258