9

Somewhat surprisingly, the identity does hold in intuitionistic logic. We give three arguments: an informal natural deduction-style proof, a formal proof in the Agda proof assistant, and a formal derivation tree in the contraction-free intuitionistic sequent calculus G4ip. Informal proof We prove the implications $\neg\neg (P \rightarrow Q) \rightarrow (\neg\...


9

You're exactly right - $A \not \vdash \perp$ means that $A$ is consistent. That is, we cannot derive a contradiction using $A$ as hypotheses. But there is a difference between "we can't prove it false" and "it's true"! Here's an easy example. Let's work with the theory of groups. Then $$ xy = yx \not \vdash \perp$$ Why is this? Because if ...


8

You can say that the hypothesis $\Gamma, A \land B$ is stronger than $\Gamma, A$ because in $\Gamma, A \land B$ you have more hypotheses than in $\Gamma, A$. But the statement $\Gamma, A \land B \vdash C$ (i.e. $C$ is derivable from the hypotheses $\Gamma, A \land B$) is weaker (in the sense of less general or less informative) than the statement $\Gamma, A \...


7

Yes, it is just a quick consequence of the elimination rule. $\to $ Elimination (in its most common phrasing) says that if $\Gamma\vdash A\to B$ and $\Gamma\vdash A$ then $\Gamma\vdash B.$ So, if $\Gamma\vdash A\to B,$ then $\Gamma, A\vdash A\to B.$ And of course $\Gamma,A\vdash A,$ so applying the elimination rule gives $\Gamma,A\vdash B.$


6

'True' refers to the English statement (2.2), 'correct' refers to the sequent $\Gamma \vdash \Psi$. The authors aim to define when a sequent is correct in a technical sense, and they use the common sense of 'true' in natural language (the meta-level). In other words, the meaning of the paragraph is that if the situation described by (2.2) holds (i.e. the ...


6

The interpretation of Γ⊢𝐴 is usually that 𝐴 is true under the assumptions in Γ. Not quite: It is "under at most the assumptions in $\Gamma$". The definition of $\vdash$ reads $\Gamma \vdash A$ iff there is a derivation $\mathcal{D}$ with end formula $A$ and $\text{Hyp}(\mathcal{D}) \subseteq \Gamma$ (where $\text{Hyp}(\mathcal{D})$ is the set ...


6

You are right: There should be a difference between $A \nvdash \bot$ and $\vdash \neg (A \to \bot)$, and there is. As you note, $A \to \bot$ is logically equivalent to/taken to be the meaning of the abbreviation $\neg A$, so $\neg(A \to \bot)$ is equivalent to $\neg \neg A$, and this is in turn equivalent to (and from which is derivable) $A$. That is, $\...


5

See : Stephen Cole Kleene, Mathematical logic (1967 - Dover reprint), page 289 : $\cfrac{A, \Gamma \to \Delta, B \quad \quad B, \Gamma \to \Delta, A}{\Gamma \to \Delta, A \equiv B} \equiv \text{: right} $ $\cfrac{A,B, \Gamma \to \Delta \quad \quad \Gamma \to \Delta, A, B}{A \equiv B, \Gamma \to \Delta} \equiv \text{: left} $ If we ...


5

The things on top are both premises... we are given both of them. So we know that if $\Gamma$ holds then $A$ or $\Delta$ does (but not which one) and also that if $\Gamma'$ and $A$ hold, then $\Delta'$ holds. Note that both of these are conditional statements. We do not need to assume (or prove) that $A$ holds. To see why the conclusion is sound given the ...


5

(red) The rule makes sense to me for ND but not for SC. In SC it says "if $\Gamma,\varphi$ proves $\Delta$ then $\neg\varphi,\Delta$". So I guess the comma on the right of $\vdash$ must be read as an OR. (And comma on the left means AND?) Yes, that's correct. From the post linked in the comments: The naive interpretation of a sequent $A_1, \ldots, ...


5

(Not too) Short answer. Yes, the rules $(Assm)$ and $(\equiv)$ are axioms. By axiom here (and in many textbooks such as Takeuti's Proof Theory cited by MauroALLEGRANZA) is intended an inference rule with no premises. In this sense, every proof system needs at least an axiom rule, otherwise there is no possibility to build a derivation: without any axiom, ...


4

I don't follow how this involves if-and-only-if. Hint A) For: if $\{ (φ_1 ∧ φ_2) \} \vdash ψ$, then $\{ φ_1, φ_2 \} \vdash ψ$. 1) $φ_1$ --- assumed 2) $φ_2$ --- assumed 3) $(φ_1 ∧ φ_2)$ --- from 1) and 2) by (∧I) So far we have: $\{ φ_1, φ_2 \} \vdash (φ_1 ∧ φ_2)$. Thus, by Sequent Rule (Transitive Rule) [page 8], from it and $\{ (φ_1 ∧ φ_2) \} \...


4

The rule you suggest is called the "mix" rule , and it is not derivable from the standard rules of linear logic. Actually, what I know is that it's not derivable in multiplicative linear logic; I can't imagine that additive or exponential rules would matter, but I don't actually know that they don't. Hyland and Ong constructed a game semantics for ...


4

Your question does not correspond to your title: actually you are asking if one can derive $\vdash \Gamma, A, A^\bot$ from $\vdash \Gamma$. It is the case if one adds the mix rule: http://llwiki.ens-lyon.fr/mediawiki/index.php/Sequent_calculus#Mix_rules Otherwise, it is not the case.


4

It depends what you mean by "logic". Is second-order logic a logic? If so, then the answer to your question is no: second-order logic has no associated sequent calculus, since it is not compact (so in particular there is no way to represent entailment in second-order logic in a finitary way). Note that there are other non-compact logics - say, infinitary ...


4

Probably your last comment about double negation elimination breaking the symmetry of natural deduction is the 'reason' for the cited quote, though I don't agree with the sentiment. Basically, natural deduction has introduction and elimination rules for each one of "$\land$" and "$\lor$" and "$\to$", which correspond to their intended meanings. We also have ...


4

Concerning the rule $\forall\text{-}L$, the intuitive meaning is the following: if under the hypotheses $\Gamma$ and $\phi[t]$ (for some term $t$) you can derive $\Delta$ (this is the premise of the rule $\forall\text{-}L$), then also under the stronger hypotheses $\Gamma$ and $\forall x \phi[x]$ you can derive $\Delta$ (this is the conclusion of the rule $\...


4

EDIT: Actually, it's way simpler than what I wrote below: clearly we have $\psi(y)\vdash\psi(y)$ but in general we don't have $\exists x(\psi(x))\vdash\psi(y)$. That is, take $\Gamma=\emptyset$ and $\Delta=\{\psi(y)\}$. Well, $\{\varphi(y),\psi(y)\}$ proves $\exists x(\varphi(x)\wedge\psi(x))$, but $\{\varphi(y), \exists x(\psi(x))\}$ doesn't. The problem ...


4

To define a logic you need to specify a language of formulas, and then you need to provide either 1) a semantics, or 2) a proof system (i.e. a collection of rules of inference). For commonly discussed logics, we usually have definitions both in terms of semantics and proof systems, and we have meta-theorems which connect specific pairs of semantics and ...


4

The Hilbert systems in that book are modular and the axioms are somewhat separable in such a way that you can obtain different systems (and fragments thereof) simply by adding or omitting axioms. For instance, in order to obtain the pure implication fragment of minimal logic Hm, you would consider only the axioms: $A\to(B\to{A})$ and $(A\to{(B\to{C})})\to{((...


4

Any instance of the axiom rule has the form $P, \Gamma \Rightarrow P$, where $P$ is an atomic formula and $\Gamma$ is a finite multiset of formulas. Possibly, $\Gamma$ contains a formula $A \land B$ or whatever formula you like. Moreover, the notation $\vdash_n \Gamma \Rightarrow C$ means that there exists a derivation with conclusion $\Gamma \Rightarrow C$ ...


4

In general, a finite sequence of $n \in \mathbb{N}$ elements in some set $K$ is commonly denoted by $(k_1, \dots, k_n)$. Note that this notation includes the case of $n = 0$ elements, where you get the empty sequence $(\ )$; and the case of $n = 1$ elements, where you get the sequence $(k_1)$. A common notation that forces a finite sequence to not be empty ...


4

When dealing with abstract representations of proofs, it is important to distinguish between hypotheses and conclusions. This is why the turnstile symbol $\vdash$ is used: on its left there are the hypotheses, on its right the conclusions. Note that the turnstile $\vdash$ is not a connective (it is not part of the object language), and the intuitive meaning ...


4

You can show that modus ponens is derivable in the sequent calculus LK. In general, an inference rule $$\dfrac{\Gamma_1 \vdash \Delta_1 \qquad \cdots \qquad \Gamma_n \vdash \Delta_n}{\Gamma \vdash \Delta}(*)$$ is derivable in LK if there is a LK derivation of the sequent $\Gamma \vdash \Delta$ starting from the premises $\Gamma_1 \vdash \Delta_1$, $\,\dots\,$...


4

No, the rules you've written are not enough. First, note that what you've written down - symmetry and transitivity - aren't enough to guarantee that $=$ ever holds. You also need reflexivity: that we're allowed to infer, from no hypotheses at all, $t_1=t_1$ for any term $t_1$. More precisely, reflexivity is the rule which allows us to infer the sequent $\...


4

The book is correct. (i) is a valid inference rule and (ii) is not valid. Also, the capital Greek letters $\Phi$ and $\Delta$ refer to sets of well-formed formulas, but $\psi$ refers to a single well-formed formula. Let's consider the two sequents $\Phi \vdash \Delta$ and $\Phi,\psi \vdash \Delta$ and consider when they are true. Also, let's define $\Phi''$ ...


3

1) I don't agree -- to respond to your initial remark -- that there are no good books teaching logic using the axiomatic method. Many classic texts do just that, famously Mendelson (which taught me serious logic, many moons ago). Of more recent axiomatic texts, Leary's Friendly Introduction is terrific. And for a book very carefully written for self-study, ...


3

I learned sequent calculus from the first couple of chapters of Takeuti's text (Proof Theory, now out of print: http://www.amazon.com/Proof-Theory-Studies-Foundations-Mathematics/dp/0444879439). I can't really compare it with other texts, but I found it worked well for me.


3

Details will depend on the system in play. But you should be able e.g. to argue from (i) $F \vdash \neg A$ to (ii) $F, A \vdash \bot$ to (iii) $F, A \vdash B$ to (iv) $F \vdash A \to B$.


3

I'll formalize Apostolos' argument with Natural Deduction in "sequent-calculus-style" [see Dirk van Dalen, Logic and Structure, (5th ed - 2013), pages 35, 88 and 91 for the rules]. These are the rules for quantifiers : $$(\forall I) \, \, {\Gamma \vdash \varphi(x) \over \Gamma \vdash \forall x \varphi(x)}\ x \notin FV(\psi) \, \text{for all} \,\, \...


Only top voted, non community-wiki answers of a minimum length are eligible