The Open Logic Text

en · official · sha256:f8c22dbe6e9e40a5050cb6913222a7c8fc8cb11a7a58f2993d90dbd7f012da70

% Part: first-order-logic % Chapter: natural-deduction % Section: derivations \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \iftag{FOL} {\olfileid{fol}{ntd}{der}} {\olfileid{pl}{ntd}{der}} \olsection{\usetoken{P}{derivation}} \begin{explain} We've said what an assumption is, and we've given the rules of inference. !!^{derivation}s in natural deduction are inductively generated from these: each !!{derivation} either is an assumption on its own, or consists of one, two, or three !!{derivation}s followed by a correct inference. \end{explain} \begin{defn}[!!^{derivation}] \Article{derivation} \emph{!!{derivation}} of !!a{sentence}~$!A$ from assumptions~$\Gamma$ is a finite tree of !!{sentence}s satisfying the following conditions: \begin{enumerate} \item The topmost !!{sentence}s of the tree are either in $\Gamma$ or are !!{discharged} by an inference in the tree. \item The bottommost !!{sentence} of the tree is~$!A$. \item Every !!{sentence} in the tree except the sentence~$!A$ at the bottom is a premise of a correct application of an inference rule whose conclusion stands directly below that !!{sentence} in the tree. \end{enumerate} We then say that $!A$ is the \emph{conclusion} of the !!{derivation} and $\Gamma$ its !!{undischarged} assumptions. If !!a{derivation} of $!A$ from~$\Gamma$ exists, we say that $!A$ is \emph{!!{derivable}} from~$\Gamma$, or in symbols: $\Gamma \Proves !A$. If there is !!a{derivation} of~$!A$ in which every assumption is !!{discharged}, we write~$\Proves !A$. \end{defn} \begin{ex} Every assumption on its own is !!a{derivation}. So, e.g., $!A$ by itself is !!a{derivation}, and so is $!B$ by itself. We can obtain a new !!{derivation} from these by applying, say, the $\Intro{\land}$ rule, \begin{prooftree} \AxiomC{$!A$} \AxiomC{$!B$} \RightLabel{\Intro{\land}} \BinaryInfC{$!A \land !B$} \end{prooftree} These rules are meant to be general: we can replace the $!A$ and~$!B$ in it with any !!{sentence}s, e.g., by $!C$ and~$!D$. Then the conclusion would be $!C \land !D$, and so \begin{prooftree} \AxiomC{$!C$} \AxiomC{$!D$} \RightLabel{\Intro{\land}} \BinaryInfC{$!C \land !D$} \end{prooftree} is a correct !!{derivation}. Of course, we can also switch the assumptions, so that $!D$ plays the role of~$!A$ and $!C$ that of~$!B$. Thus, \begin{prooftree} \AxiomC{$!D$} \AxiomC{$!C$} \RightLabel{\Intro{\land}} \BinaryInfC{$!D \land !C$} \end{prooftree} is also a correct !!{derivation}. We can now apply another rule, say, $\Intro{\lif}$, which allows us to conclude a conditional and allows us to !!{discharge} any assumption that is identical to the antecedent of that conditional. So both of the following would be correct !!{derivation}s: \begin{prooftree} \AxiomC{$\Discharge{!C}{1}$} \AxiomC{$!D$} \RightLabel{\Intro{\land}} \BinaryInfC{$!C \land !D$} \DischargeRule{\Intro{\lif}}{1} \UnaryInfC{$!C \lif (!C \land !D)$} \DisplayProof\bottomAlignProof \AxiomC{$!C$} \AxiomC{$\Discharge{!D}{1}$} \RightLabel{\Intro{\land}} \BinaryInfC{$!C \land !D$} \DischargeRule{\Intro{\lif}}{1} \UnaryInfC{$!D \lif (!C \land !D)$} \end{prooftree} They show, respectively, that $!D \Proves !C \lif (!C \land !D)$ and $!C \Proves !D \lif (!C \land !D)$. Remember that discharging of assumptions is a permission, not a requirement: we don't have to discharge the assumptions. In particular, we can apply a rule even if the assumptions are not present in the !!{derivation}. For instance, the following is legal, even though there is no assumption~$!A$ to be !!{discharged}: \begin{prooftree} \AxiomC{$!B$} \DischargeRule{\Intro{\lif}}{1} \UnaryInfC{$!A \lif !B$} \end{prooftree} \end{ex} \end{document}

en · official · sha256:065989fd1223eefe2ee2c013a7d2d90fdd4bb7a57d814f34a01800b96d9e056c

\subsection{Rules for $\land$} \begin{defish} \AxiomC{$!A$} \AxiomC{$!B$} \RightLabel{\Intro{\land}} \BinaryInfC{$!A \land !B$} \DisplayProof \hfill \begin{tabular}{r} \AxiomC{$!A \land !B$} \RightLabel{\Elim{\land}} \UnaryInfC{$!A$} \DisplayProof \\[3ex] \AxiomC{$!A \land !B$} \RightLabel{\Elim{\land}} \UnaryInfC{$!B$} \DisplayProof \end{tabular} \end{defish}

Referencing norms: ND_AND_E1, ND_AND_E2, ND_AND_I, S_ANDE_C1, S_ANDE_C2, S_ANDE_P, S_ANDE_PL, S_ANDE_PR, S_ANDI_C, S_ANDI_CL, S_ANDI_CR, S_ANDI_P1, S_ANDI_P2, V_ANDE_A, V_ANDE_B, V_ANDI_A, V_ANDI_B

en · official · sha256:66567438cbee4cd9e83593333a55aedadcebae58c3ef1c22f60f41bcd3b2c74c

\subsection{Rules for $\lfalse$} \begin{defish} \AxiomC{$\lfalse$} \RightLabel{\FalseInt} \UnaryInfC{$!A$} \DisplayProof \hfill \AxiomC{$\Discharge{\lnot !A}{n}$} \DeduceC{$\lfalse$} \DischargeRule{\FalseCl}{n} \UnaryInfC{$!A$} \DisplayProof \end{defish} Note that $\Intro{\lnot}$ and $\FalseCl$ are very similar: The difference is that $\Intro{\lnot}$ derives a negated !!{sentence}~$\lnot !A$ but $\FalseCl$ a positive !!{sentence}~$!A$. Whenever a rule indicates that some assumption may be discharged, we take this to be a permission, but not a requirement. E.g., in the $\Intro{\lif}$ rule, we may discharge any number of assumptions of the form~$!A$ in the !!{derivation} of the premise~$!B$, including zero.

Referencing norms: ND_FALSE_C, ND_FALSE_I, P_CLASSICAL_REDUCTIO, S_FALSEC_ASSUMPTION, S_FALSEC_ASSUMPTION_A, S_FALSEC_C, S_FALSEC_P, S_FALSEI_C, S_FALSEI_P, V_FALSEC_A, V_FALSEI_A

en · official · sha256:9fea93c37af083a883d3c257332ef56dd5dd6aa1af1d8e2715251ec0688a01ed

\subsection{Rules for $\lif$} \begin{defish} \AxiomC{$\Discharge{!A}{n}$} \DeduceC{$!B$} \DischargeRule{\Intro{\lif}}{n} \UnaryInfC{$!A \lif !B$} \DisplayProof \hfill \AxiomC{$!A \lif !B$} \AxiomC{$!A$} \RightLabel{\Elim{\lif}} \BinaryInfC{$!B$} \DisplayProof \end{defish}

Referencing norms: ND_IF_E, ND_IF_I, S_IFE_C, S_IFE_P1, S_IFE_P2, S_IFE_P2L, S_IFE_P2R, S_IFI_ASSUMPTION, S_IFI_C, S_IFI_CL, S_IFI_CR, S_IFI_P1, V_IFE_A, V_IFE_B, V_IFI_A, V_IFI_B

en · official · sha256:b13d45e8f7c45c7543cb3c061ef69a9b6af6ce5772455f7e4444513c833cac01

\subsection{Rules for $\lnot$} \begin{defish} \AxiomC{$\Discharge{!A}{n}$} \noLine \DeduceC{$\lfalse$} \DischargeRule{\Intro{\lnot}}{n} \UnaryInfC{$\lnot !A$} \DisplayProof \hfill \AxiomC{$\lnot !A$} \AxiomC{$!A$} \RightLabel{\Elim{\lnot}} \BinaryInfC{$\lfalse$} \DisplayProof \end{defish}

Referencing norms: ND_NOT_E, ND_NOT_I, S_NOTI_ASSUMPTION, S_NOTI_C, S_NOTI_CA, S_NOTI_P, V_NOTI_A

en · official · sha256:0c9edb66ce94c3c2d62723f658384684736ca1360e5d5bf3d07f463b4594cce8

\subsection{Rules for $\lor$} \begin{defish} \begin{tabular}{r} \AxiomC{$!A$} \RightLabel{\Intro{\lor}} \UnaryInfC{$!A \lor !B$} \DisplayProof \\[3ex] \AxiomC{$!B$} \RightLabel{\Intro{\lor}} \UnaryInfC{$!A \lor !B$} \DisplayProof \end{tabular} \hfill \AxiomC{$!A \lor !B$} \AxiomC{$\Discharge{!A}{n}$} \DeduceC{$!C$} \AxiomC{$\Discharge{!B}{n}$} \DeduceC{$!C$} \DischargeRule{\Elim{\lor}}{n} \TrinaryInfC{$!C$} \DisplayProof \end{defish}

Referencing norms: ND_OR_E, ND_OR_I1, ND_OR_I2, S_ORE_ASSUMPTION_A, S_ORE_ASSUMPTION_B, S_ORE_C, S_ORE_P1, S_ORE_P1L, S_ORE_P1R, S_ORE_P2, S_ORE_P3, V_ORE_A, V_ORE_B, V_ORE_C

en · official · sha256:2414476549184213ac7cd8d164ff59ee13707873990067af4e07e905faf5e5f7

\subsection{Rules for $\lexists$} \begin{defish} \AxiomC{$\Atom{!A}{t}$} \RightLabel{\Intro{\lexists}} \UnaryInfC{$\lexists[x][\Atom{!A}{x}]$} \DisplayProof \hfill \AxiomC{$\lexists[x][\Atom{!A}{x}]$} \AxiomC{[$\Atom{!A}{a}$]$^n$} \DeduceC{$!C$} \DischargeRule{\Elim{\lexists}}{n} \BinaryInfC{$!C$} \DisplayProof \end{defish} Again, $t$ is a closed term, and $a$ is !!a{constant} which does not occur in the premise $\lexists[x][!A(x)]$, in the conclusion~$!C$, or any assumption which is !!{undischarged} in the !!{derivation}s ending with the two premises (other than the assumptions $!A(a)$). We call $a$ the \emph{eigenvariable} of the \Elim{\lexists} inference. The condition that an eigenvariable neither occur in the premises nor in any assumption that is !!{undischarged} in the !!{derivation}s leading to the premises for the \Intro{\lforall} or \Elim{\lexists} inference is called the \emph{eigenvariable condition}. \begin{explain} Recall the convention that when $!A$ is !!a{formula} with the !!{variable}~$x$ free, we indicate this by writing~$!A(x)$. In the same context, $!A(t)$ then is short for~$\Subst{!A}{t}{x}$. So we could also write the $\Intro\lexists$ rule as: \begin{prooftree} \AxiomC{$\Subst{!A}{t}{x}$} \RightLabel{\Intro{\lexists}} \UnaryInfC{$\lexists[x][!A]$} \end{prooftree} Note that $t$ may already occur in~$!A$, e.g., $!A$~might be~$\Atom{\Obj P}{t,x}$. Thus, inferring $\lexists[x][\Atom{\Obj P}{t,x}]$ from~$\Atom{\Obj P}{t,t}$ is a correct application of~$\Intro\lexists$---you may ``replace'' one or more, and not necessarily all, occurrences of~$t$ in the premise by the bound !!{variable}~$x$. However, the eigenvariable conditions in $\Intro\lforall$ and~$\Elim\lexists$ require that the !!{constant}~$a$ does not occur in~$!A$. So, you cannot correctly infer $\lforall[x][\Atom{\Obj P}{a,x}]$ from $\Atom{\Obj P}{a,a}$ using~$\Intro\lforall$. \end{explain} \begin{explain} In \Intro{\lexists} and \Elim{\lforall} there are no restrictions, and the term~$t$ can be anything, so we do not have to worry about any conditions. On the other hand, in the \Elim{\lexists} and \Intro{\lforall} rules, the eigenvariable condition requires that the !!{constant}~$a$ does not occur anywhere in the conclusion or in an !!{undischarged} assumption. The condition is necessary to ensure that the system is sound, i.e., only !!{derive}s !!{sentence}s from !!{undischarged} assumptions from which they follow. Without this condition, the following would be allowed: \begin{prooftree} \AxiomC{$\lexists[x][!A(x)]$} \AxiomC{$\Discharge{!A(a)}{1}$} \RightLabel{*\Intro{\lforall}} \UnaryInfC{$\lforall[x][!A(x)]$} \RightLabel{\Elim{\lexists}} \BinaryInfC{$\lforall[x][!A(x)]$} \end{prooftree} However, $\lexists[x][!A(x)] \Entails/ \lforall[x][!A(x)]$. As the elimination rules for quantifiers only allow substituting closed terms for !!{variable}s, it follows that any !!{formula} that can be derived from a set of !!{sentence}s is itself !!a{sentence}. \end{explain}

Referencing norms: ND_EX_E, ND_EX_I, S_EXE_ASSUMPTION, S_EXE_ASSUMPTION_A, S_EXE_C, S_EXE_P1, S_EXE_P1A, S_EXE_P2, V_EXE_A, V_EXE_C

en · official · sha256:44ed13e20a358e48bf22e7d52c6522a1836415304bfebbe1d012e20895742948

\subsection{Rules for $\lforall$} \begin{defish} \AxiomC{$!A(a)$} \RightLabel{\Intro{\lforall}} \UnaryInfC{$\lforall[x][\Atom{!A}{x}]$} \DisplayProof \hfill \AxiomC{$\lforall[x][\Atom{!A}{x}]$} \RightLabel{\Elim{\lforall}} \UnaryInfC{$!A(t)$} \DisplayProof \end{defish} In the rules for~$\lforall$, $t$ is a closed term (a term that does not contain any variables), and $a$~is !!a{constant} which does not occur in the conclusion~$\lforall[x][!A(x)]$, or in any assumption which is !!{undischarged} in the !!{derivation} ending with the premise~$!A(a)$. We call $a$ the \emph{eigenvariable} of the \Intro{\lforall} inference.\footnote{We use the term ``eigenvariable'' even though $a$ in the above rule is a constant. This has historical reasons.}

Referencing norms: ND_ALL_E, ND_ALL_I, S_ALLI_C, S_ALLI_CA, S_ALLI_P, S_ALLI_PA, V_ALLI_A

en · official · sha256:bd9f903c5492585f55edf162170929f4e42bde79e469c682dafe1445994a8c95

% Part: first-order-logic % Chapter: natural-deduction % Section: rules-and-proofs \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \iftag{FOL} {\olfileid{fol}{ntd}{rul}} {\olfileid{pl}{ntd}{rul}} \olsection{Rules and \usetoken{P}{derivation}} \begin{explain} Natural deduction systems are meant to closely parallel the informal reasoning used in mathematical proof (hence it is somewhat ``natural''). Natural deduction proofs begin with assumptions. Inference rules are then applied. Assumptions are ``!!{discharged}'' by the \Intro{\lnot}, \Intro{\lif}, \iftag{FOL}{\Elim{\lor} and \Elim{\lexists}}{ and \Elim{\lor}} inference rules, and the label of the !!{discharged} assumption is placed beside the inference for clarity. \end{explain} \begin{defn}[Assumption] An \emph{assumption} is any !!{sentence} in the topmost position of any branch. \end{defn} !!^{derivation}s in natural deduction are certain trees of !!{sentence}s, where the topmost !!{sentence}s are assumptions, and if !!a{sentence} stands below one, two, or three other sequents, it must follow correctly by a rule of inference. The !!{sentence}s at the top of the inference are called the \emph{premises} and the !!{sentence} below the \emph{conclusion} of the inference. The rules come in pairs, an introduction and an elimination rule for each !!{operator}. They introduce !!a{operator} in the conclusion or remove !!a{operator} from a premise of the rule. Some of the rules allow an assumption of a certain type to be \emph{!!{discharged}}. To indicate which assumption is !!{discharged} by which inference, we also assign labels to both the assumption and the inference. This is indicated by writing the assumption as ``$\Discharge{!A}{n}$.'' % Only include this sentence is on of \land, lor, lif or lnot is defined. \iftag{notprvNot,notprvAnd,notprvOr,notprvIf}{}% {It is customary to consider rules for all the !!{operator}s $\land$, $\lor$, $\lif$, $\lnot$, and $\lfalse$, even if some of those are defined.} \end{document}

Referencing norms: ReadingAvailable, context_form, reading_available, rule_reading

en · official · sha256:e89032908259a7c9124723f0a88746fee1b276ebcd753a5cea23dcb76d241e3e

% Part: first-order-logic % Chapter: proof-systems % Section: introduction \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \iftag{FOL} {\olfileid{fol}{prf}{int}} {\olfileid{pl}{prf}{int}} \olsection{Introduction} Logics commonly have both a semantics and !!a{derivation} system. The semantics concerns concepts such as truth, satisfiability, validity, and entailment. The purpose of !!{derivation} systems is to provide a purely syntactic method of establishing entailment and validity. They are purely syntactic in the sense that a !!{derivation} in such a system is a finite syntactic object, usually a sequence (or other finite arrangement) of !!{sentence}s or !!{formula}s. Good !!{derivation} systems have the property that any given sequence or arrangement of !!{sentence}s or !!{formula}s can be verified mechanically to be ``correct.'' The simplest (and historically first) !!{derivation} systems for first-order logic were \emph{axiomatic}. A sequence of !!{formula}s counts as !!a{derivation} in such a system if each individual !!{formula} in it is either among a fixed set of ``axioms'' or follows from !!{formula}s coming before it in the sequence by one of a fixed number of ``inference rules''---and it can be mechanically verified if !!a{formula} is an axiom and whether it follows correctly from other !!{formula}s by one of the inference rules. Axiomatic !!{derivation} systems are easy to describe---and also easy to handle meta-theoretically---but !!{derivation}s in them are hard to read and understand, and are also hard to produce. Other !!{derivation} systems have been developed with the aim of making it easier to construct !!{derivation}s or easier to understand !!{derivation}s once they are complete. Examples are natural deduction, truth trees, also known as tableaux proofs, and the sequent calculus. Some !!{derivation} systems are designed especially with mechanization in mind, e.g., the resolution method is easy to implement in software (but its !!{derivation}s are essentially impossible to understand). Most of these other !!{derivation} systems represent !!{derivation}s as trees of !!{formula}s rather than sequences. This makes it easier to see which parts of !!a{derivation} depend on which other parts. So for a given logic, such as first-order logic, the different !!{derivation} systems will give different explications of what it is for !!a{sentence} to be a \emph{theorem} and what it means for !!a{sentence} to be !!{derivable} from some others. However that is done (via axiomatic !!{derivation}s, natural deductions, sequent !!{derivation}s, truth trees, resolution refutations), we want these relations to match the semantic notions of validity and entailment. Let's write $\Proves !A$ for ``$!A$~is a theorem'' and ``$\Gamma \Proves !A$'' for ``$!A$~is !!{derivable} from~$\Gamma$.'' However $\Proves$~is defined, we want it to match up with $\Entails$, that is: \begin{enumerate} \item $\Proves !A$ if and only if $\Entails !A$ \item $\Gamma \Proves !A$ if and only if $\Gamma \Entails !A$ \end{enumerate} The ``only if'' direction of the above is called \emph{soundness}. !!^a{derivation} system is sound if !!{derivability} guarantees entailment (or validity). Every decent !!{derivation} system has to be sound; unsound !!{derivation} systems are not useful at all. After all, the entire purpose of !!a{derivation} is to provide a syntactic guarantee of validity or entailment. We'll prove soundness for the !!{derivation} systems we present. The converse ``if'' direction is also important: it is called \emph{completeness}. A complete !!{derivation} system is strong enough to show that $!A$~is a theorem whenever $!A$~is valid, and that $\Gamma \Proves !A$ whenever $\Gamma \Entails !A$. Completeness is harder to establish, and some logics have no complete !!{derivation} systems. First-order logic does. Kurt G\"odel was the first one to prove completeness for !!a{derivation} system of first-order logic in his 1929 dissertation. Another concept that is connected to !!{derivation} systems is that of \emph{consistency}. A set of !!{sentence}s is called inconsistent if anything whatsoever can be !!{derive}d from it, and consistent otherwise. Inconsistency is the syntactic counterpart to unsatisfiablity: like unsatisfiable sets, inconsistent sets of !!{sentence}s do not make good theories, they are defective in a fundamental way. Consistent sets of !!{sentence}s may not be true or useful, but at least they pass that minimal threshold of logical usefulness. For different !!{derivation} systems the specific definition of consistency of sets of !!{sentence}s might differ, but like~$\Proves$, we want consistency to coincide with its semantic counterpart, satisfiability. We want it to always be the case that $\Gamma$ is consistent if and only if it is satisfiable. Here, the ``only if'' direction amounts to completeness (consistency guarantees satisfiability), and the ``if'' direction amounts to soundness (satisfiability guarantees consistency). In fact, for classical first-order logic, the two versions of soundness and completeness are equivalent. \end{document}

Referencing norms: CalculusDescribed, CorrespondingBackward, CorrespondingForward, ExpressesStep, ForeignRuleByEmptyMembership, RuleHasHome, STEP_IMPLICATION_PROOF, STEP_IMPLICATION_USE, calculus_described, calculus_shape, corresponding_rules, expresses_step, foreign_rule, rule_has_home, same_step_as

en · official · sha256:56f530f197551df3ae11f40c8093313d7aad1888d30f3511f6e72ddbef22091e

% Part: first-order-logic % Chapter: proof-systems % Section: natural-deduction \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \iftag{FOL} {\olfileid{fol}{prf}{ntd}} {\olfileid{pl}{prf}{ntd}} \olsection{Natural Deduction} Natural deduction is !!a{derivation} system intended to mirror actual reasoning (especially the kind of regimented reasoning employed by mathematicians). Actual reasoning proceeds by a number of ``natural'' patterns. For instance, proof by cases allows us to establish a conclusion on the basis of a disjunctive premise, by establishing that the conclusion follows from either of the disjuncts. Indirect proof allows us to establish a conclusion by showing that its negation leads to a contradiction. Conditional proof establishes a conditional claim ``if \dots then \dots'' by showing that the consequent follows from the antecedent. Natural deduction is a formalization of some of these natural inferences. Each of the logical connectives and quantifiers comes with two rules, an introduction and an elimination rule, and they each correspond to one such natural inference pattern. For instance, $\Intro{\lif}$ corresponds to conditional proof, and $\Elim{\lor}$ to proof by cases. A particularly simple rule is $\Elim{\land}$ which allows the inference from $!A \land !B$ to~$!A$ (or $!B$). One feature that distinguishes natural deduction from other !!{derivation} systems is its use of assumptions. !!^a{derivation} in natural deduction is a tree of !!{formula}s. A single !!{formula} stands at the root of the tree of !!{formula}s, and the ``leaves'' of the tree are !!{formula}s from which the conclusion is derived. In natural deduction, some leaf !!{formula}s play a role inside the !!{derivation} but are ``used up'' by the time the !!{derivation} reaches the conclusion. This corresponds to the practice, in actual reasoning, of introducing hypotheses which only remain in effect for a short while. For instance, in a proof by cases, we assume the truth of each of the disjuncts; in conditional proof, we assume the truth of the antecedent; in indirect proof, we assume the truth of the negation of the conclusion. This way of introducing hypothetical assumptions and then doing away with them in the service of establishing an intermediate step is a hallmark of natural deduction. The formulas at the leaves of a natural deduction !!{derivation} are called assumptions, and some of the rules of inference may ``!!{discharge}'' them. For instance, if we have !!a{derivation} of~$!B$ from some assumptions which include~$!A$, then the $\Intro{\lif}$ rule allows us to infer~$!A \lif !B$ and discharge any assumption of the form~$!A$. (To keep track of which assumptions are discharged at which inferences, we label the inference and the assumptions it discharges with a number.) The assumptions that remain !!{undischarged} at the end of the !!{derivation} are together sufficient for the truth of the conclusion, and so !!a{derivation} establishes that its !!{undischarged} assumptions entail its conclusion. The relation $\Gamma \Proves !A$ based on natural deduction holds iff there is !!a{derivation} in which $!A$~is the last !!{sentence} in the tree, and every leaf which is !!{undischarged} is in~$\Gamma$. $!A$~is a theorem in natural deduction iff there is !!a{derivation} in which $!A$~is the last !!{sentence} and all assumptions are !!{discharged}. For instance, here is !!a{derivation} that shows that $\Proves (!A \land !B) \lif !A$: \begin{prooftree} \AxiomC{$\Discharge{!A \land !B}{1}$} \RightLabel{\Elim{\land}} \UnaryInfC{$!A$} \DischargeRule{\Intro{\lif}}{1} \UnaryInfC{$(!A \land !B) \lif !A$} \end{prooftree} The label~$1$ indicates that the assumption $!A \land !B$ is !!{discharged} at the \Intro{\lif} inference. A set~$\Gamma$ is inconsistent iff $\Gamma \Proves \lfalse$ in natural deduction. The rule \FalseInt{} makes it so that from an inconsistent set, any !!{sentence} can be !!{derive}d. Natural deduction systems were developed by Gerhard Gentzen and Stanis\l{}aw Ja\'skowski in the 1930s, and later developed by Dag Prawitz and Frederic Fitch. Because its inferences mirror natural methods of proof, it is favored by philosophers. The versions developed by Fitch are often used in introductory logic textbooks. In the philosophy of logic, the rules of natural deduction have sometimes been taken to give the meanings of the logical operators (``proof-theoretic semantics''). \end{document}

Referencing norms: ND

en · official · sha256:40face3555dd40d16832da3fd34b6d8445b4297dcb8cdbf8d2e11f770ef36fdf

% Part: first-order-logic % Chapter: proof-systems % Section: seqeunt-calculus \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \iftag{FOL} {\olfileid{fol}{prf}{seq}} {\olfileid{pl}{prf}{seq}} \olsection{The Sequent Calculus} While many !!{derivation} systems operate with arrangements of !!{sentence}s, the sequent calculus operates with \emph{sequents}. A sequent is an expression of the form \[ !A_1, \dots, !A_m \Sequent !B_1, \dots, !B_m, \] that is a pair of sequences of !!{sentence}s, separated by the sequent symbol~$\Sequent$. Either sequence may be empty. !!^a{derivation} in the sequent calculus is a tree of sequents, where the topmost sequents are of a special form (they are called ``initial sequents'' or ``axioms'') and every other sequent follows from the sequents immediately above it by one of the rules of inference. The rules of inference either manipulate the !!{sentence}s in the sequents (adding, removing, or rearranging them on either the left or the right), or they introduce a complex !!{formula} in the conclusion of the rule. For instance, the $\LeftR{\land}$ rule allows the inference from $!A, \Gamma \Sequent \Delta$ to $!A \land !B, \Gamma \Sequent \Delta$, and the $\RightR{\lif}$ allows the inference from $!A, \Gamma \Sequent \Delta, !B$ to $\Gamma \Sequent \Delta, !A \lif !B$, for any $\Gamma$, $\Delta$, $!A$, and~$!B$. (In particular, $\Gamma$ and~$\Delta$ may be empty.) The $\Proves$ relation based on the sequent calculus is defined as follows: $\Gamma \Proves !A$ iff there is some sequence $\Gamma_0$ such that every $!A$ in $\Gamma_0$ is in~$\Gamma$ and there is a !!{derivation} with the sequent~$\Gamma_0 \Sequent !A$ at its root. $!A$ is a theorem in the sequent calculus if the sequent~$\Sequent !A$ has !!a{derivation}. For instance, here is !!a{derivation} that shows that $\Proves (!A \land !B) \lif !A$: \begin{prooftree} \Axiom$!A \fCenter !A$ \RightLabel{\LeftR{\land}} \UnaryInf$!A \land !B \fCenter !A$ \RightLabel{\RightR{\lif}} \UnaryInf$\fCenter (!A \land !B) \lif !A$ \end{prooftree} A set $\Gamma$ is inconsistent in the sequent calculus if there is !!a{derivation} of $\Gamma_0 \Sequent$ (where every $!A \in \Gamma_0$ is in~$\Gamma$ and the right side of the sequent is empty). Using the rule \RightR{\Weakening}, any !!{sentence} can be !!{derive}d from an inconsistent set. The sequent calculus was invented in the 1930s by Gerhard Gentzen. Because of its systematic and symmetric design, it is a very useful formalism for developing a theory of !!{derivation}s. It is relatively easy to find !!{derivation}s in the sequent calculus, but these !!{derivation}s are often hard to read and their connection to proofs are sometimes not easy to see. It has proved to be a very elegant approach to !!{derivation} systems, however, and many logics have sequent calculus systems. \end{document}

en · official · sha256:7359c02106b7d83cbb23c2d21b0c1a78cdf4a770297a9e8e503e4091e2580eb3

% Part: first-order-logic % Chapter: proof-systems % Section: tableaux \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \iftag{FOL} {\olfileid{fol}{prf}{tab}} {\olfileid{pl}{prf}{tab}} \olsection{\usetoken{P}{tableau}} While many !!{derivation} systems operate with arrangements of !!{sentence}s, !!{tableau}s operate with !!{signed formula}s. !!^a{signed formula} is a pair consisting of a truth value sign ($\True$ or $\False$) and !!a{sentence} \[ \sFmla{\True}{!A} \text{ or } \sFmla{\False}{!A}. \] !!^a{tableau} consists of !!{signed formula}s arranged in a downward-branching tree. It begins with a number of \emph{assumptions} and continues with !!{signed formula}s which result from one of the !!{signed formula}s above it by applying one of the rules of inference. Each rule allows us to add one or more !!{signed formula}s to the end of a branch, or two !!{signed formula}s side by side---in this case a branch splits into two, with the two added !!{signed formula}s forming the ends of the two branches. A rule applied to a complex !!{signed formula} results in the addition of !!{signed formula}s which are immediate sub-!!{formula}s. They come in pairs, one rule for each of the two signs. For instance, the $\TRule{\True}{\land}$ rule applies to $\sFmla{\True}{!A \land !B}$, and allows the addition of both the two !!{signed formula}s $\sFmla{\True}{!A}$ and~$\sFmla{\True}{!B}$ to the end of any branch containing $\sFmla{\True}{!A \land !B}$, and the rule $\TRule{\False}{!A \land !B}$ allows a branch to be split by adding $\sFmla{\False}{!A}$ and $\sFmla{\False}{!B}$ side-by-side. !!^a{tableau} is closed if every one of its branches contains a matching pair of !!{signed formula}s $\sFmla{\True}{!A}$ and $\sFmla{\False}{!A}$. The $\Proves$ relation based on !!{tableau}s is defined as follows: $\Gamma \Proves !A$ iff there is some finite set~$\Gamma_0 = \{!B_1, \dots, !B_n\} \subseteq \Gamma$ such that there is a closed !!{tableau} for the assumptions \[ \{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\} \] For instance, here is a closed !!{tableau} that shows that $\Proves (!A \land !B) \lif !A$: \begin{oltableau} [\sFmla{\False}{(\formula{A} \land \formula{B}) \lif \formula{A}}, just = \TAss [\sFmla{\True}{\formula{A} \land \formula{B}}, just = {\TRule{\False}{\lif}[1]} [\sFmla{\False}{\formula{A}}, just = {\TRule{\False}{\lif}[1]} [\sFmla{\True}{\formula{A}}, just = {\TRule{\True}{\lif}[2]} [\sFmla{\True}{\formula{B}}, just = {\TRule{\True}{\lif}[2]}, close] ] ] ] ] \end{oltableau} A set $\Gamma$ is inconsistent in the !!{tableau} calculus if there is a closed !!{tableau} for assumptions \[ \{\sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\} \] for some $!B_i \in \Gamma$. !!^{tableau}s were invented in the 1950s independently by Evert Beth and Jaakko Hintikka, and simplified and popularized by Raymond Smullyan. They are very easy to use, since constructing !!a{tableau} is a very systematic procedure. Because of the systematic nature of !!{tableau}s, they also lend themselves to implementation by computer. However, !!a{tableau} is often hard to read and their connection to proofs are sometimes not easy to see. The approach is also quite general, and many different logics have !!{tableau} systems. !!^{tableau}s also help us to find !!{structure}s that satisfy given (sets of) !!{sentence}s: if the set is satisfiable, it won't have a closed !!{tableau}, i.e., any !!{tableau} will have an open branch. The satisfying !!{structure} can be ``read off'' an open branch, provided every rule it is possible to apply has been applied on that branch. There is also a very close connection to the sequent calculus: essentially, a closed !!{tableau} is a condensed !!{derivation} in the sequent calculus, written upside-down. \end{document}

en · official · sha256:d7b53ee88b84746cb4113a4e3ec2583a0c633360f8145fa83ff3771b8bd1f86e

% Part: first-order-logic % Chapter: sequent-calculus % Section: propositional-rules \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \iftag{FOL} {\olfileid{fol}{seq}{prl}} {\olfileid{pl}{seq}{prl}} \olsection{Propositional Rules} \subsection{Rules for $\lnot$} \begin{defish} \Axiom$ \Gamma \fCenter \Delta, !A $ \RightLabel{\LeftR{\lnot}} \UnaryInf$ \lnot !A, \Gamma \fCenter \Delta$ \DisplayProof \hfill \Axiom$!A, \Gamma \fCenter \Delta$ \RightLabel{\RightR{\lnot}} \UnaryInf$ \Gamma \fCenter \Delta, \lnot !A $ \DisplayProof \end{defish} \subsection{Rules for $\land$} \begin{defish}\noindent \begin{tabular}{l} \Axiom$ !A, \Gamma \fCenter \Delta$ \RightLabel{\LeftR{\land}} \UnaryInf$ !A \land !B, \Gamma \fCenter \Delta$ \DisplayProof \\[3ex] \Axiom$!B, \Gamma \fCenter \Delta$ \RightLabel{\LeftR{\land}} \UnaryInf$!A \land !B, \Gamma \fCenter \Delta$ \DisplayProof \end{tabular} \hfill \Axiom$\Gamma \fCenter \Delta, !A$ \Axiom$ \Gamma \fCenter \Delta, !B$ \RightLabel{\RightR{\land}} \BinaryInf$ \Gamma \fCenter \Delta, !A \land !B $ \DisplayProof \end{defish} \subsection{Rules for $\lor$} \begin{defish} \Axiom$!A, \Gamma \fCenter \Delta$ \Axiom$!B, \Gamma \fCenter \Delta$ \RightLabel{\LeftR{\lor}} \BinaryInf$!A \lor !B, \Gamma \fCenter \Delta$ \DisplayProof \hfill \begin{tabular}{r} \Axiom$\Gamma \fCenter \Delta, !A$ \RightLabel{\RightR{\lor}} \UnaryInf$ \Gamma \fCenter \Delta, !A \lor !B$ \DisplayProof \\[3ex] \Axiom$ \Gamma \fCenter \Delta, !B$ \RightLabel{\RightR{\lor}} \UnaryInf$ \Gamma \fCenter \Delta, !A \lor !B$ \DisplayProof \end{tabular} \end{defish} \subsection{Rules for $\lif$} \begin{defish} \Axiom$ \Gamma \fCenter \Delta, !A$ \Axiom$ !B, \Pi \fCenter \Lambda$ \RightLabel{\LeftR{\lif}} \BinaryInf$ !A \lif !B, \Gamma, \Pi \fCenter \Delta, \Lambda$ \DisplayProof \hfill \Axiom$ !A, \Gamma \fCenter \Delta, !B$ \RightLabel{\RightR{\lif}} \UnaryInf$ \Gamma \fCenter \Delta, !A \lif !B $ \DisplayProof \end{defish} \end{document}

en · official · sha256:62280bdf4536bcf7caeee1a6f52c888e7813465bedac236663ff77e612123041

% Part: first-order-logic % Chapter: sequent-calculus % Section: quantifier-rules \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{seq}{qrl} \olsection{Quantifier Rules} \subsection{Rules for $\lforall$} \begin{defish} \Axiom$ !A(t), \Gamma \fCenter \Delta$ \RightLabel{\LeftR{\lforall}} \UnaryInf$ \lforall[x][!A(x)],\Gamma \fCenter \Delta$ \DisplayProof \hfill \Axiom$ \Gamma \fCenter \Delta, !A(a) $ \RightLabel{\RightR{\lforall}} \UnaryInf$ \Gamma \fCenter \Delta, \lforall[x][!A(x)]$ \DisplayProof \end{defish} In \LeftR{\lforall}, $t$ is a closed term (i.e., one without variables). In \RightR{\lforall}, $a$~is !!a{constant} which must not occur anywhere in the lower sequent of the \RightR{\lforall} rule. We call $a$ the \emph{eigenvariable} of the \RightR{\forall} inference.\footnote{We use the term ``eigenvariable'' even though $a$ in the above rule is !!a{constant}. This has historical reasons.} \subsection{Rules for $\lexists$} \begin{defish} \Axiom$ !A(a), \Gamma \fCenter \Delta $ \RightLabel{\LeftR{\lexists}} \UnaryInf$ \lexists[x][!A(x)], \Gamma \fCenter \Delta$ \DisplayProof \hfill \Axiom$ \Gamma \fCenter \Delta, !A(t) $ \RightLabel{\RightR{\lexists}} \UnaryInf$ \Gamma \fCenter \Delta, \lexists[x][!A(x)]$ \DisplayProof \end{defish} Again, $t$~is a closed term, and $a$~is !!a{constant} which does not occur in the lower sequent of the \LeftR{\lexists} rule. We call $a$ the \emph{eigenvariable} of the \LeftR{\lexists} inference. The condition that an eigenvariable not occur in the lower sequent of the \RightR{\lforall} or \LeftR{\lexists} inference is called the \emph{eigenvariable condition}. \begin{explain} Recall the convention that when $!A$ is !!a{formula} with the !!{variable}~$x$ free, we indicate this by writing~$!A(x)$. In the same context, $!A(t)$ then is short for~$\Subst{!A}{t}{x}$. So we could also write the \RightR{\lexists} rule as: \begin{prooftree} \Axiom$\Gamma \fCenter \Delta, \Subst{!A}{t}{x}$ \RightLabel{\RightR{\lexists}} \UnaryInf$\Gamma \fCenter \Delta, \lexists[x][!A]$ \end{prooftree} Note that $t$ may already occur in~$!A$, e.g., $!A$~might be~$\Atom{\Obj P}{t,x}$. Thus, inferring $\Gamma \Sequent \Delta, \lexists[x][\Atom{\Obj P}{t,x}]$ from~$\Gamma \Sequent \Delta, \Atom{\Obj P}{t,t}$ is a correct application of~\RightR{\lexists}---you may ``replace'' one or more, and not necessarily all, occurrences of~$t$ in the premise by the bound !!{variable}~$x$. However, the eigenvariable conditions in \RightR{\lforall} and~\LeftR{\lexists} require that the !!{constant}~$a$ does not occur in~$!A$. So, you cannot correctly infer $\Gamma \Sequent \Delta, \lforall[x][\Atom{\Obj P}{a,x}]$ from $\Gamma \Sequent \Delta, \Atom{\Obj P}{a,a}$ using~$\RightR{\lforall}$. \end{explain} \begin{explain} In \RightR{\lexists} and \LeftR{\lforall} there are no restrictions on the term~$t$. On the other hand, in the \LeftR{\lexists} and \RightR{\lforall} rules, the eigenvariable condition requires that the !!{constant}~$a$ does not occur anywhere outside of~$!A(a)$ in the upper sequent. It is necessary to ensure that the system is sound, i.e., only !!{derive}s sequents that are valid. Without this condition, the following would be allowed: \begin{prooftree} \Axiom$!A(a) \fCenter !A(a)$ \RightLabel{*\LeftR{\lexists}} \UnaryInf$\lexists[x][!A(x)] \fCenter !A(a)$ \RightLabel{\RightR{\lforall}} \UnaryInf$\lexists[x][!A(x)] \fCenter \lforall[x][!A(x)]$ \DisplayProof\bottomAlignProof \qquad \Axiom$!A(a) \fCenter !A(a)$ \RightLabel{*\RightR{\lforall}} \UnaryInf$!A(a) \fCenter \lforall[x][!A(x)]$ \RightLabel{\LeftR{\lexists}} \UnaryInf$\lexists[x][!A(x)] \fCenter \lforall[x][!A(x)]$ \end{prooftree} However, $\lexists[x][!A(x)] \Sequent \lforall[x][!A(x)]$ is not valid. \end{explain} \end{document}

en · official · sha256:9348a4e24e201a098fc81faa792adf61bf3de7a841a6de3aa5fc7d5c2434c133

% Part: first-order-logic % Chapter: sequent-calculus % Section: rules-and-proofs \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \iftag{FOL} {\olfileid{fol}{seq}{rul}} {\olfileid{pl}{seq}{rul}} \olsection{Rules and \usetoken{P}{derivation}} For the following, let $\Gamma, \Delta, \Pi, \Lambda$ represent finite sequences of !!{sentence}s. \begin{defn}[Sequent] A \emph{sequent} is an expression of the form \[ \Gamma \Sequent \Delta \] where $\Gamma$ and $\Delta$ are finite (possibly empty) sequences of !!{sentence}s of the language $\Lang L$. $\Gamma$ is called the \emph{antecedent}, while $\Delta$ is the \emph{succedent}. \end{defn} \begin{explain} The intuitive idea behind a sequent is: if all of the !!{sentence}s in the antecedent hold, then at least one of the !!{sentence}s in the succedent holds. That is, if $\Gamma = \tuple{!A_1, \dots, !A_m}$ and $\Delta = \tuple{!B_1, \dots, !B_n}$, then $\Gamma \Sequent \Delta$ holds iff \[ (!A_1 \land \cdots \land !A_m) \lif (!B_1 \lor \cdots \lor !B_n) \] holds. There are two special cases: where $\Gamma$ is empty and when $\Delta$~is empty. When $\Gamma$ is empty, i.e., $m = 0$, $\quad \Sequent \Delta$ holds iff $!B_1 \lor \dots \lor !B_n$ holds. When $\Delta$ is empty, i.e., $n = 0$, $\Gamma \Sequent \quad$ holds iff $\lnot(!A_1 \land \dots \land !A_m)$ does. We say a sequent is valid iff the corresponding !!{sentence} is valid. \end{explain} If $\Gamma$ is a sequence of !!{sentence}s, we write $\Gamma, !A$ for the result of appending $!A$ to the right end of~$\Gamma$ (and $!A, \Gamma$ for the result of appending $!A$ to the left end of~$\Gamma$). If $\Delta$ is a sequence of !!{sentence}s also, then $\Gamma, \Delta$ is the concatenation of the two sequences. \begin{defn}[Initial Sequent] An \emph{initial sequent} is a sequent \iftag{prvFalse,prvTrue}{of one of the following forms: \begin{enumerate} \item $!A \Sequent !A$ \tagitem{prvTrue}{$\quad \Sequent \ltrue$}{} \tagitem{prvFalse}{$\lfalse \Sequent \quad$}{} \end{enumerate}} {of the form $!A \Sequent !A$} for any !!{sentence} $!A$ in the language. \end{defn} !!^{derivation}s in the sequent calculus are certain trees of sequents, where the topmost sequents are initial sequents, and if a sequent stands below one or two other sequents, it must follow correctly by a rule of inference. The rules for $\Log{LK}$ are divided into two main types: \emph{logical} rules and \emph{structural} rules. The logical rules are named for the !!{main operator} of the !!{sentence} containing $!A$ and/or $!B$ in the lower sequent. Each one comes in two versions, one for inferring a sequent with the !!{sentence} containing the !!{operator} on the left, and one with the !!{sentence} on the right. \end{document}

en · official · sha256:97d10d8b0cf55cea36e42a3182d089a6155ddd9d90ae529d531fb12c9573abad

% Part: first-order-logic % Chapter: sequent-calculus % Section: structural-rules \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \iftag{FOL} {\olfileid{fol}{seq}{srl}} {\olfileid{pl}{seq}{srl}} \olsection{Structural Rules} We also need a few rules that allow us to rearrange !!{sentence}s in the left and right side of a sequent. Since the logical rules require that the !!{sentence}s in the premise which the rule acts upon stand either to the far left or to the far right, we need an ``exchange'' rule that allows us to move !!{sentence}s to the right position. It's also important sometimes to be able to combine two identical !!{sentence}s into one, and to add !!a{sentence} on either side. \subsection{Weakening} \begin{defish} \Axiom$ \Gamma \fCenter \Delta $ \RightLabel{\LeftR{\Weakening}} \UnaryInf$ !A, \Gamma \fCenter \Delta$ \DisplayProof \hfill \Axiom$ \Gamma \fCenter \Delta$ \RightLabel{\RightR{\Weakening}} \UnaryInf$ \Gamma \fCenter \Delta, !A$ \DisplayProof \end{defish} \subsection{Contraction} \begin{defish} \Axiom$ !A, !A, \Gamma \fCenter \Delta $ \RightLabel{\LeftR{\Contraction}} \UnaryInf$ !A, \Gamma \fCenter \Delta$ \DisplayProof \hfill \Axiom$ \Gamma \fCenter \Delta, !A, !A$ \RightLabel{\RightR{\Contraction}} \UnaryInf$ \Gamma \fCenter \Delta, !A$ \DisplayProof \end{defish} \subsection{Exchange} \begin{defish} \Axiom$ \Gamma, !A, !B, \Pi \fCenter \Delta $ \RightLabel{\LeftR{\Exchange}} \UnaryInf$ \Gamma, !B, !A, \Pi \fCenter \Delta$ \DisplayProof \hfill \Axiom$ \Gamma \fCenter \Delta, !A, !B, \Lambda$ \RightLabel{\RightR{\Exchange}} \UnaryInf$ \Gamma \fCenter \Delta, !B, !A, \Lambda$ \DisplayProof \end{defish} A series of weakening, contraction, and exchange inferences will often be indicated by double inference lines. The following rule, called ``cut,'' is not strictly speaking necessary, but makes it a lot easier to reuse and combine !!{derivation}s. \begin{defish} \[ \Axiom$ \Gamma \fCenter \Delta, !A$ \Axiom$ !A, \Pi \fCenter \Lambda $ \RightLabel{\Cut} \BinaryInf$ \Gamma, \Pi \fCenter \Delta, \Lambda$ \DisplayProof \] \end{defish} \end{document}

en · official · sha256:dc97c91f7f593272b13f016a9644d472b20f0909d21ea0d8aafd8f7f83bd3d84

\subsection{Rules for $\land$} \begin{defish}\noindent \AxiomC{\sFmla{\True}{!A \land !B}} \RightLabel{\TRule{\True}{\land}} \UnaryInfC{\sFmla{\True}{!A}} \noLine \UnaryInfC{\sFmla{\True}{!B}} \DisplayProof \hfill \AxiomC{\sFmla{\False}{!A \land !B}} \RightLabel{\TRule{\False}{\land}} \UnaryInfC{$\sFmla{\False}{!A} \quad \mid \quad \sFmla{\False}{!B}$} \DisplayProof \end{defish}

en · official · sha256:664a7dad8f4154cc4d52ff69e3a399a3bbaa521dbe422b1675a7dfd0e97d3884

\subsection{Rules for $\lif$} \begin{defish} \AxiomC{\sFmla{\True}{!A \lif !B}} \RightLabel{\TRule{\True}{\lif}} \UnaryInfC{$\sFmla{\False}{!A} \quad \mid \quad \sFmla{\True}{!B}$} \DisplayProof \hfill \AxiomC{\sFmla{\False}{!A \lif !B}} \RightLabel{\TRule{\False}{\lif}} \UnaryInfC{\sFmla{\True}{!A}} \noLine \UnaryInfC{\sFmla{\False}{!B}} \DisplayProof \end{defish}

Referencing norms: S_TABIF_C1, S_TABIF_C1A, S_TABIF_C2, S_TABIF_C2B, S_TABIF_P, S_TABIF_PA, S_TABIF_PB, S_TABIF_PF, TAB_IF_FALSE, TAB_IF_TRUE, V_TABIF_A, V_TABIF_B

en · official · sha256:2031cf011e36b9e117e597391069c0ee4814be84cbab1778e2f81faef0942d9a

\subsection{Rules for $\lnot$} \begin{defish} \AxiomC{\sFmla{\True}{\lnot !A}} \RightLabel{\TRule{\True}{\lnot}} \UnaryInfC{\sFmla{\False}{!A}} \DisplayProof \hfill \AxiomC{\sFmla{\False}{\lnot !A}} \RightLabel{\TRule{\False}{\lnot}} \UnaryInfC{\sFmla{\True}{!A}} \DisplayProof \end{defish}

en · official · sha256:018a7a41773f929dc5a0995a08f414785c94e19e5f27efd9b31928912d225647

\subsection{Rules for $\lor$} \begin{defish} \AxiomC{\sFmla{\True}{!A \lor !B}} \RightLabel{\TRule{\True}{\lor}} \UnaryInfC{$\sFmla{\True}{!A} \quad \mid \quad \sFmla{\True}{!B}$} \DisplayProof \hfill \AxiomC{\sFmla{\False}{!A \lor !B}} \RightLabel{\TRule{\False}{\lor}} \UnaryInfC{\sFmla{\False}{!A}} \noLine \UnaryInfC{\sFmla{\False}{!B}} \DisplayProof \end{defish}

en · official · sha256:2e78dd80fd6bf062d58b86182914794299a0b643e88be785002f65b4e648d634

\subsection{The Cut Rule} \begin{defish} \AxiomC{} \RightLabel{\Cut} \UnaryInfC{$\sFmla{\True}{!A} \quad \mid \quad \sFmla{\False}{!A}$} \DisplayProof \end{defish} The \Cut{} rule is not applied ``to'' a previous !!{signed formula}; rather, it allows every branch in !!a{tableau} to be split in two, one branch containing $\sFmla{\True}{!A}$, the other~$\sFmla{\False}{!A}$. It is not necessary---any set of !!{signed formula}s with a closed !!{tableau} has one not using \Cut---but it allows us to combine !!{tableau}s in a convenient way.

Referencing norms: TAB_CUT

en · official · sha256:e0aa8fa03e935a69a6bb617619d1b521b1e1e569a570fb23298293caaac9b546

% Part: first-order-logic % Chapter: tableaux % Section: quantifier-rules \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{tab}{qrl} \olsection{Quantifier Rules} \subsection{Rules for $\lforall$} \begin{defish} \AxiomC{\sFmla{\True}{\lforall[x][!A(x)]}} \RightLabel{\TRule{\True}{\forall}} \UnaryInfC{\sFmla{\True}{!A(t)}} \DisplayProof \hfill \AxiomC{\sFmla{\False}{\lforall[x][!A(x)]}} \RightLabel{\TRule{\False}{\lforall}} \UnaryInfC{\sFmla{\False}{!A(a)}} \DisplayProof \end{defish} In \TRule{\True}{\lforall}, $t$ is a closed term (i.e., one without variables). In \TRule{\False}{\lforall}, $a$~is !!a{constant} which must not occur anywhere in the branch above \TRule{\False}{\lforall} rule. We call $a$ the \emph{eigenvariable} of the \TRule{\False}{\forall} inference.\footnote{We use the term ``eigenvariable'' even though $a$ in the above rule is !!a{constant}. This has historical reasons.} \subsection{Rules for $\lexists$} \begin{defish} \AxiomC{\sFmla{\True}{\lexists[x][!A(x)]}} \RightLabel{\TRule{\True}{\lexists}} \UnaryInfC{\sFmla{\True}{!A(a)}} \DisplayProof \hfill \AxiomC{\sFmla{\False}{\lexists[x][!A(x)]}} \RightLabel{\TRule{\False}{\lexists}} \UnaryInfC{\sFmla{\False}{!A(t)}} \DisplayProof \end{defish} Again, $t$~is a closed term, and $a$~is !!a{constant} which does not occur in the branch above the~\TRule{\True}{\lexists} rule. We call $a$ the \emph{eigenvariable} of the \TRule{\True}{\lexists} inference. The condition that an eigenvariable not occur in the branch above the \TRule{\False}{\lforall} or \TRule{\True}{\lexists} inference is called the \emph{eigenvariable condition}. \begin{explain} Recall the convention that when $!A$ is !!a{formula} with the !!{variable}~$x$ free, we indicate this by writing~$!A(x)$. In the same context, $!A(t)$ then is short for~$\Subst{!A}{t}{x}$. So we could also write the \TRule{\False}{\lexists} rule as: \begin{prooftree} \AxiomC{\sFmla{\False}{\lexists[x][!A]}} \RightLabel{\TRule{\False}{\lexists}} \UnaryInfC{\sFmla{\False}{\Subst{!A}{t}{x}}} \end{prooftree} Note that $t$ may already occur in~$!A$, e.g., $!A$~might be~$\Atom{\Obj P}{t,x}$. Thus, inferring $\sFmla{\False}{\Atom{\Obj P}{t,t}}$ from~$ \sFmla{\False}{\lexists[x][\Atom{\Obj P}{t,x}]}$ is a correct application of~\TRule{\False}{\lexists}. However, the eigenvariable conditions in \TRule{\False}{\lforall} and~\TRule{\True}{\lexists} require that the !!{constant}~$a$ does not occur in~$!A$. So, you cannot correctly infer $\sFmla{\False}{\Atom{\Obj P}{a,a}}$ from $\sFmla{\False}{\lforall[x][\Atom{\Obj P}{a,x}]}$ using~$\TRule{\False}{\lforall}$. \end{explain} \begin{explain} In \TRule{\True}{\lforall} and \TRule{\False}{\lexists} there are no restrictions on the term~$t$. On the other hand, in the \TRule{\True}{\lexists} and \TRule{\False}{\lforall} rules, the eigenvariable condition requires that the !!{constant}~$a$ does not occur anywhere in the branches above the respective inference. It is necessary to ensure that the system is sound. Without this condition, the following would be a closed !!{tableau} for $\lexists[x][\formula{A}(x)] \lif \lforall[x][\formula{A}(x)]$: \begin{center} \begin{tableau}{} [\sFmla{\False}{\lexists[x][\formula{A}(x)] \lif \lforall[x][\formula{A}(x)]}, just=\TAss [\sFmla{\True}{\lexists[x][\formula{A}(x)]}, just={\TRule{\False}{\lif}[1]} [\sFmla{\False}{\lforall[x][\formula{A}(x)]}, just={\TRule{\False}{\lif}[1]} [\sFmla{\True}{\formula{A}(a)}, just={\TRule{\True}{\lexists}[2]} [\sFmla{\False}{\formula{A}(a)}, just={\TRule{\False}{\lforall}[3]}, close] ] ] ] ] \end{tableau} \end{center} However, $\lexists[x][\formula{A}(x)] \lif \lforall[x][\formula{A}(x)]$ is not valid. \end{explain} \end{document}

en · official · sha256:99d3f8155fa3f8630e8a324d8dbf5bb231ade72a72a538697ada4f7ffbf20c20

% Part: first-order-logic % Chapter: tableaux % Section: rules-and-proofs \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \iftag{FOL} {\olfileid{fol}{tab}{rul}} {\olfileid{pl}{tab}{rul}} \olsection{Rules and \usetoken{P}{tableau}} !!^a{tableau} is a systematic survey of the possible ways !!a{sentence} can be true or false in !!a{structure}. The building blocks of a tableau are !!{signed formula}s: !!{sentence}s plus a truth value ``sign,'' either $\True$ or~$\False$. These signed !!{formula}s are arranged in a (downward growing) tree. \begin{defn} A \emph{!!{signed formula}} is a pair consisting of a truth value and !!a{sentence}, i.e., either: \[ \sFmla{\True}{!A} \text{ or } \sFmla{\False}{!A}. \] \end{defn} Intuitively, we might read $\sFmla{\True}{!A}$ as ``$!A$ might be true'' and $\sFmla{\False}{!A}$ as ``$!A$ might be false'' (in some !!{structure}). Each !!{signed formula} in the tree is either an \emph{assumption} (which are listed at the very top of the tree), or it is obtained from !!a{signed formula} above it by one of a number of rules of inference. There are two rules for each possible !!{main operator} of the preceding !!{formula}, one for the case where the sign is~$\True$, and one for the case where the sign is~$\False$. Some rules allow the tree to branch, and some only add !!{signed formula}s to the branch. A rule may be (and often must be) applied not to the immediately preceding !!{signed formula}, but to any !!{signed formula} in the branch from the root to the place the rule is applied. A branch is \emph{closed} when it contains both $\sFmla{\True}{!A}$ and $\sFmla{\False}{!A}$. A closed !!{tableau} is one where every branch is closed. Under the intuitive interpretation, any branch describes a joint possibility, but $\sFmla{\True}{!A}$ and $\sFmla{\False}{!A}$ are not jointly possible. In other words, if a branch is closed, the possibility it describes has been ruled out. In particular, that means that a closed !!{tableau} rules out all possibilities of simultaneously making every assumption of the form $\sFmla{\True}{!A}$ true and every assumption of the form~$\sFmla{\False}{!A}$ false. A closed !!{tableau} \emph{for $!A$} is a closed !!{tableau} with root~$\sFmla{\False}{!A}$. If such a closed !!{tableau} exists, all possibilities for~$!A$ being false have been ruled out; i.e., $!A$ must be true in every !!{structure}. \end{document}

Referencing norms: CLOSED_BRANCH, SIGNED_FORMULA, TABLEAU, termination_condition

en · official · sha256:03b84170662d6af10403a31c1f4cda1bba2201438535811fe491d0132a46f213

\subsection{Absurdity} \begin{defish} \AxiomC{$\lfalse$} \RightLabel{\FalseInt} \UnaryInfC{$!A$} \DisplayProof \end{defish} If we have !!a{derivation} of~$\lfalse$ from !!{undischarged} assumptions~$!B_1$, \dots, $!B_n$, then there is a function~$f(M_1, \dots, M_n)$ that turns constructions of $!B_1$, \dots, $!B_n$ into a construction of~$\lfalse$. Since $\lfalse$ has no construction, there cannot be any constructions of all of $!B_1$, \dots, $!B_n$ either. Hence, $f$ also has the property that \emph{if} $M_1$, \dots, $M_n$ are constructions of $!B_1$, \dots, $!B_n$, respectively, \emph{then} $f(M_1, \dots, M_n)$ is a construction of~$!A$.

Referencing norms: NDI, P_EX_FALSO

en · official · sha256:92a721b71306f1d85828f0ee459ed5e2fb561e747b1d212c7995c4a4c1e2d690

\subsection{Conditional} \begin{defish} \AxiomC{$\Discharge{!A}{u}$} \DeduceC{$!B$} \DischargeRule{$\Intro{\lif}$}{u} \UnaryInfC{$!A \lif !B$} \DisplayProof \hfill \AxiomC{$!A \lif !B$} \AxiomC{$!A$} \RightLabel{$\Elim{\lif}$} \BinaryInfC{$!B$} \DisplayProof \end{defish} If we have !!a{derivation} of~$!B$ from !!{undischarged} assumption~$!A$, then there is a function~$f$ that turns constructions of~$!A$ into constructions of~$!B$. That same function is a construction of $!A \lif !B$. So, if the premise of $\Intro\lif$ has a construction conditional on a construction of~$!A$, the conclusion $!A \lif !B$ has a construction. On the other hand, suppose there are constructions~$N$ of $!A$ and $f$ of $!A \lif !B$. A construction of $!A \lif !B$ is a function that turns constructions of $!A$ into constructions of~$!B$. So, $f(N)$ is a construction of~$!B$, i.e., the conclusion of $\Elim\lif$ has a construction.

en · official · sha256:076e4873b3bfd73d45d18f4e6525823f840d00f6ac415916a46a07ace0f1e8cd

\subsection{Conjunction} \begin{defish} \AxiomC{$!A$} \AxiomC{$!B$} \RightLabel{\Intro{\land}} \BinaryInfC{$!A \land !B$} \DisplayProof \hfill \begin{tabular}{l} \AxiomC{$!A \land !B$} \RightLabel{\Elim{\land}} \UnaryInfC{$!A$} \DisplayProof \\[3ex] \AxiomC{$!A \land !B$} \RightLabel{\Elim{\land}} \UnaryInfC{$!B$} \DisplayProof \end{tabular} \end{defish} Suppose we have constructions $N_1$, $N_2$ of $!A_1$ and $!A_2$, respectively. Then we also have a construction $!A_1 \land !A_2$, namely the pair $\tuple{N_1, N_2}$. A construction of $!A_1 \land !A_1$ on the BHK interpretation is a pair $\tuple{N_1, N_2}$. So assume we have such a pair. Then we also have a construction of each conjunct: $N_1$ is a construction of~$!A_1$ and $N_2$ is a construction of $!A_2$.

en · official · sha256:184152be3ada223a0322ba41fad5fdbe49125afa76a288fc3f5505bdecd347c0

\subsection{Disjunction} \begin{defish} \begin{tabular}{l} \AxiomC{$!A$} \RightLabel{\Intro{\lor}} \UnaryInfC{$!A \lor !B$} \DisplayProof \\[3ex] \AxiomC{$!B$} \RightLabel{\Intro{\lor}} \UnaryInfC{$!A \lor !B$} \DisplayProof \end{tabular} \hfill \AxiomC{$!A \lor !B$} \AxiomC{$\Discharge{!A}{n}$} \DeduceC{$!C$} \AxiomC{$\Discharge{!B}{n}$} \DeduceC{$!C$} \DischargeRule{\Elim{\lor}}{n} \TrinaryInfC{$!C$} \DisplayProof \end{defish} If we have a construction~$N_i$ of~$!A_i$ we can turn it into a construction~$\tuple{i, N_i}$ of~$!A_1 \lor !A_2$. On the other hand, suppose we have a construction of~$!A_1 \lor !A_2$, i.e., a pair $\tuple{i, N_i}$ where $N_i$ is a construction of~$!A_i$, and also functions $f_1$, $f_2$, which turn constructions of $!A_1$, $!A_2$, respectively, into constructions of~$!C$. Then $f_i(N_i)$ is a construction of~$!C$, the conclusion of~$\Elim\lor$.

en · official · sha256:b39bc6522ac949d16ec2c3e062f75c0154460eee6af0f05dbbe47126b87fcbd1

\subsection{Rules for $\lnot$} Since $\lnot !A$ is defined as $!A \lif \lfalse$, we strictly speaking do not need rules for~$\lnot$. But if we did, this is what they'd look like: \begin{defish} \AxiomC{$\Discharge{!A}{n}$} \noLine \DeduceC{$\lfalse$} \DischargeRule{\Intro{\lnot}}{n} \UnaryInfC{$\lnot !A$} \DisplayProof \hfill \AxiomC{$\lnot !A$} \AxiomC{$!A$} \RightLabel{\Elim{\lnot}} \BinaryInfC{$\lfalse$} \DisplayProof \end{defish}

en · official · sha256:b23007a09bbf7b4b8390943539aab59ee00277b3af8450b5d07142eaf9d1af10

% Part: proof-theory % Chapter: sequent-calculus % Section: admissible-derivable \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{pt}{seq}{adm} \olsection{Admissible and Derivable Rules} Many results of proof theory concern---or use---results about whether everything that can be !!{prove}d using a specific rule can also be !!{prove}d without that rule. The cut-elimination theorem is the most well-known example. It shows that any sequent that can be !!{prove}d using the rules of a sequent system with~\Cut{} can also be !!{prove}d without~\Cut. Because this kind of property is so important, it has a name. \begin{defn} A rule~$R$ is \emph{admissible} in a sequent system if any sequent that can be proved in that system together with the rule~$R$ can also be proved without~$R$. \end{defn} \begin{ex}\ollabel{ex:land-deriv} The rule $\LeftR{\land}$ takes different forms in \Log{G1c} and \Log{G3c}. In \Log{G1c} there are two versions of the rule, one with the left conjunct $!A$ of the principal !!{formula}~$!A \land !B$ in the premise, and one with the right conjunct~$!B$: \[ \Axiom$ !A, \Gamma \fCenter \Delta$ \RightLabel{$\LeftR{\land}_1$} \UnaryInf$ !A \land !B, \Gamma \fCenter \Delta$ \DisplayProof \qquad \Axiom$!B, \Gamma \fCenter \Delta$ \RightLabel{$\LeftR{\land}_2$} \UnaryInf$!A \land !B, \Gamma \fCenter \Delta$ \DisplayProof \] By contrast, \Log{G3c} has only one rule: \[ \Axiom$ !A, !B, \Gamma \fCenter \Delta$ \RightLabel{$\LeftR{\land}_3$} \UnaryInf$ !A \land !B, \Gamma \fCenter \Delta$ \DisplayProof \] We might now ask, ``Is \Log{G3c}'s rule $\LeftR{\land}_3$ admissible in \Log{G1c}?'' It is: we can directly simulate any inference using $\LeftR{\land}_3$ using only the rules of~\Log{G1c}. In addition to $\LeftR{\land}_1$ and $\LeftR{\land}_2$ we'll also need the structural rule~$\LeftR{\Contraction}$: \[ \Axiom$!A, !B, \Gamma \fCenter \Delta$ \RightLabel{$\LeftR{\land}_1$} \UnaryInf$!A \land !B, !B, \Gamma \fCenter \Delta$ \RightLabel{$\LeftR{\land}_2$} \UnaryInf$!A \land !B, !A \land !B, \Gamma \fCenter \Delta$ \RightLabel{\LeftR{\Contraction}} \UnaryInf$!A \land !B \Gamma \fCenter \Delta$ \DisplayProof \] \end{ex} Simulating a inferences using one rule using other rules is one way to show that a rule is admissible. But it is not the only way, and some rules are admissible but can't be so simulated. Rules that can be are called \emph{derivable}. \begin{defn} A rule~$R$, \[ \AxiomC{$S_1$} \AxiomC{$\dots$} \AxiomC{$S_n$} \RightLabel{$R$} \TrinaryInfC{$S$} \DisplayProof \] is called \emph{derivable} in a system if there is a schematic !!{proof} of the sequent~$S$ using the rules and axioms of the system together with additional initial sequents of the forms of~$S_1$, \dots,~$S_n$. \end{defn} The !!{proof} given in \olref{ex:land-deriv} shows that $\LeftR{\land}_3$ is a derivable rule in~\Log{G1c}, as that !!{proof} is a schematic !!{proof} of the conclusion of $\LeftR{\land}_3$ from the premises of $\LeftR{\land}_3$ as initial sequents using only rules of \Log{G1c}. (It didn't use any of the axioms of \Log{G1c}.) \begin{prop}\ollabel{prop:lor-G3-adm} The rules $\LeftR{\land}$ and $\RightR{\lor}$ of~\Log{G3c} are derivable in~\Log{G1c}. \end{prop} \begin{proof} The proof for $\LeftR{\land}$ is given in \olref{ex:land-deriv}. The proof for $\RightR{\lor}$ is left as an exercise. \end{proof} \begin{prob} Show that the rule $\RightR{\lor}$ of \Log{G3c} is derivable in~\Log{G1c}. \end{prob} \begin{prob} Suppose $\liff$ is a defined !!{operator}: $!A \liff !B$ is short for $(!A \lif !B) \land (!B \lif !A)$. Show that the rules \begin{enumerate} \item \Axiom$\Gamma, !A, !B \fCenter \Delta$ \Axiom$\Gamma \fCenter \Delta, !A, !B$ \RightLabel{\LeftR{\liff}} \BinaryInf$\Gamma \fCenter \Delta, !A \liff !B$ \DisplayProof \item \Axiom$!A, \Gamma \fCenter \Delta, !B$ \Axiom$!B, \Gamma \fCenter \Delta, !A$ \RightLabel{\RightR{\liff}} \BinaryInf$\Gamma \fCenter \Delta, !A \liff !B$ \DisplayProof \end{enumerate} are derivable in (a)~\Log{G1c} and (b)~\Log{G3c}. \end{prob} \begin{ex}\ollabel{ex:weak-adm} The rule $\RightR{\Weakening}$ of \Log{G1c}, \[ \Axiom$ \Gamma \fCenter \Delta$ \RightLabel{\RightR{\Weakening}} \UnaryInf$ \Gamma \fCenter \Delta, !A$ \DisplayProof \] is admissible in~\Log{G3c}. The idea of the proof is simple: suppose there is !!a{proof}~$\pi$ of the premise $\Gamma \Sequent \Delta$ in~\Log{G3c}. Add the !!{formula}~$!A$ to the succedent of every sequent in~$\pi$. Axioms remain axioms; correct inferences are still correct inferences. The end-!!{formula} of the new !!{proof} is $\Gamma \Sequent \Delta, !A$. The rule $\RightR{\Weakening}$ is, however, not derivable in~\Log{G3c}. For suppose it were, i.e., suppose one could find !!a{proof} of $\Gamma \Sequent \Delta, !A$ using only the axioms and rules of~\Log{G3c} plus possibly the additional initial sequent~$\Gamma \Sequent \Delta$. If this !!{proof} is, as would be required for $\RightR{\Weakening}$ to be derivable, purely schematic, we could turn it into !!a{proof} of~$\Sequent !A$ by deleting $\Gamma$ and~$\Delta$. This would turn the additional initial sequents~$\Gamma \Sequent \Delta$ into the empty sequent~$\quad \Sequent \quad$. Since the empty sequent contains no !!{formula}s at all, but all rules of~\Log{G3c} require at least one active !!{formula} in their premises, the empty sequent can't be a premise of any inference in this schematic !!{proof}. Consequently, the !!{proof} can only be schematic if it doesn't actually use the additional sequent $\Gamma \Sequent \Delta$ as an initial sequent. In other words, it would be a schematic derivation of $\Gamma \Sequent \Delta, !A$ using only the axioms and rules of~\Log{G3c} and we would have shown that any sequent of this form has !!a{proof} in~\Log{G3c}. But this is impossible, since \Log{G3c} is sound and so can only !!{prove} sequents that are true in every !!{structure}. Taking $\Gamma = \Delta = \emptyset$ and $!A \ident \lfalse$, \Log{G3c} would have to !!{prove}, e.g., the sequent $\quad \Sequent \lfalse$, which it does not. \end{ex} Let's give a nice inductive proof of the result that weakening is an admissible rule in~\Log{G3c}. In fact, a slightly stronger result holds, as the intuitive argument shows: by adding $!A$ to the right side of every sequent of~$\pi$, we do not change the structure of the !!{proof}, in particular, we do not increase the height. Since this is important, it deserves its own definition. \begin{defn} A rule~$R$, \[ \AxiomC{$S_1$} \AxiomC{$\dots$} \AxiomC{$S_n$} \RightLabel{$R$} \TrinaryInfC{$S$} \DisplayProof \] is \emph{!!{height}-preserving admissible} (or \emph{!!{hp}-admissible}) in a system if, whenever $\Proves[h_i] S_i$ for $i = 1$, \dots,~$n$, then $\Proves_m S$ with $m = \max(h_1, \dots, h_n)$. \end{defn} Note that it is enough for a rule to be !!{height}-preserving admissable that, whenever the premises~$S_i$ have !!{proof}s~$\pi_i$ with !!{height}~$h_i = \pheight{\pi_i}$, there is !!a{proof}~$\pi$ of the conclusion of !!{height}~$\pheight{\pi}$ no greater than the maximum of the~$h_i$. In particular, if there is only one premise~$S_1$, it is enough that $\pheight{\pi} \le \pheight{\pi_1}$. In the case of $\RightR{\Weakening}$ and $\LeftR{\Weakening}$ we actually have $\pheight{\pi} = \pheight{\pi_1}$, but that is not necessary. \begin{prop}\ollabel{prop:weak-G3c-adm} The rules $\RightR{\Weakening}$ and $\LeftR{\Weakening}$ of \Log{G1c} are !!{height}-preserving admissible in~\Log{G3c}. \end{prop} \begin{proof} We have to show that if $\Log{G3c} \Proves \Gamma \Sequent \Delta$ with a !!{proof}~$\pi$ of !!{height}~$\pheight{\pi} = n$ then there is a \Log{G3c}-!!{proof} $\pi'$ of $\Gamma \Sequent \Delta, !A$ with $\pheight{\pi'} = n$. We prove this by induction on~$n$. If $n=0$, then $\pi$ is just the axiom $\Gamma \Sequent \Delta$ (i.e., some atomic $!C$ occurs in both $\Gamma$ and~$\Delta$), and so is $\Gamma \Sequent \Delta, !A$. If $n = \pheight{\pi} >0$, the !!{proof}~$\pi$ has a last inference. We distinguish cases according to which rule was used. We give just one example: suppose the last inference was $\RightR{\land}$. Then $\Delta = \Delta', !B \land !C$ and the immediate sub-!!{proof}s $\pi_1$ and~$\pi_2$ of the last inference have end-sequents $\Gamma \Sequent \Delta', !B$ and $\Gamma \Sequent \Delta', !C$, respectively. In other words, $\pi$ looks like this: \[ \AxiomC{} \RightLabel{$\pi_1$} \Deduce$\Gamma \fCenter \Delta', !B$ \AxiomC{} \RightLabel{$\pi_2$} \Deduce$\Gamma \fCenter \Delta', !C$ \RightLabel{\RightR{\land}} \BinaryInf$\Gamma \fCenter \Delta', !B \land !C$ \DisplayProof \] We also have that $n = \max(\pheight{\pi_1}, \pheight{\pi_2}) + 1$. So $\pheight{\pi_1} < n$ and $\pheight{\pi_2} < n$, and the inductive hypothesis applies: there are !!{proof}s $\pi_1'$ and~$\pi_2'$ of $\Gamma \Sequent \Delta', !B, !A$ and $\Gamma \Sequent \Delta', !C, !A$. Using the $\RightR{\land}$ rule, we obtain !!a{proof}~$\pi'$ of $\Gamma \Sequent \Delta', !B \land !C, !A$: \[ \AxiomC{} \RightLabel{$\pi_1'$} \Deduce$\Gamma \fCenter \Delta', !B, !A$ \AxiomC{} \RightLabel{$\pi_2'$} \Deduce$\Gamma \fCenter \Delta', !C, !A$ \RightLabel{\RightR{\land}} \BinaryInf$\Gamma \fCenter \Delta', !B \land !C, !A$ \DisplayProof \] We have $\pheight{\pi'} = \max(\pheight{\pi_1'}, \pheight{\pi_2'}) + 1 = \max(\pheight{\pi_1}, \pheight{\pi_2}) + 1 = \pheight{\pi}$. \end{proof} \olref{prop:weak-G3c-adm} is extremely useful. We'll introduce a notation for repeated application of it: if $\pi$ is !!a{proof} of~$\Gamma \Sequent \Delta$ then $\pi[\Pi \Sequent \Lambda]$ is the result of applying admissibility of weakening on the left with all the !!{formula}s in~$\Pi$ and admissibility of weakening on the right with all !!{formula}s in~$\Lambda$. It is !!a{proof} of $\Gamma, \Pi \Sequent \Delta, \Lambda$. \end{document}

Referencing norms: AdmissibleRule, BasicRule, DerivableIsAdmissible, DerivableRule, G3C, G3C_AND_L, admissible_rule_of, basic_rule_of, derivable_rule_of

en · official · sha256:5f0e90b89f32fc32abbaec69c7107cee02e2ddc297d4c1837b40beb121b9c790

% Part: proof-theory % Chapter: sequent-calculus % Section: rules-G3c \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \begin{table} \begin{tabular}{@{}c@{}c@{}} \multicolumn{2}{@{}c@{}}{Axioms}\\[2ex] $!C, \Gamma \Sequent !C$ & $\lfalse, \Gamma \Sequent \Delta$ \\[2ex] \multicolumn{2}{@{}c@{}}{Logical Rules}\\[2ex] \Axiom$\lnot !A, \Gamma \fCenter !A $ \RightLabel{\LeftR{\lnot}} \UnaryInf$\lnot !A, \Gamma \fCenter \Delta$ \DisplayProof & \Axiom$!A, \Gamma \fCenter$ \RightLabel{\RightR{\lnot}} \UnaryInf$ \Gamma \fCenter \lnot !A $ \DisplayProof \\[4ex] \Axiom$ !A, !B, \Gamma \fCenter \Delta$ \RightLabel{\LeftR{\land}} \UnaryInf$ !A \land !B, \Gamma \fCenter \Delta$ \DisplayProof & \Axiom$\Gamma \fCenter !A$ \Axiom$ \Gamma \fCenter !B$ \RightLabel{\RightR{\land}} \BinaryInf$ \Gamma \fCenter !A \land !B $ \DisplayProof \\[4ex]\Axiom$!A, \Gamma \fCenter \Delta$ \Axiom$!B, \Gamma \fCenter \Delta$ \RightLabel{\LeftR{\lor}} \BinaryInf$!A \lor !B, \Gamma \fCenter \Delta$ \DisplayProof & \begin{tabular}[t]{@{}r@{}} \Axiom$\Gamma \fCenter \Delta, !A$ \RightLabel{\RightR{\lor}} \UnaryInf$ \Gamma \fCenter \Delta, !A \lor !B$ \DisplayProof \\[3ex] \Axiom$ \Gamma \fCenter \Delta, !B$ \RightLabel{\RightR{\lor}} \UnaryInf$ \Gamma \fCenter \Delta, !A \lor !B$ \DisplayProof\\[3ex] \end{tabular} \\[4ex] \Axiom$!A \lif !B, \Gamma \fCenter !A$ \Axiom$!B, \Gamma \fCenter \Delta$ \RightLabel{\LeftR{\lif}} \BinaryInf$!A \lif !B, \Gamma \fCenter \Delta$ \DisplayProof & \Axiom$!A, \Gamma \fCenter !B$ \RightLabel{\RightR{\lif}} \UnaryInf$ \Gamma \fCenter !A \lif !B $ \DisplayProof \\[4ex] \Axiom$ !A(t), \lforall[x][!A(x)]\Gamma \fCenter \Delta$ \RightLabel{\LeftR{\lforall}} \UnaryInf$ \lforall[x][!A(x)],\Gamma \fCenter \Delta$ \DisplayProof & \Axiom$ \Gamma \fCenter !A(a) $ \RightLabel{\RightR{\lforall}} \UnaryInf$ \Gamma \fCenter \lforall[x][!A(x)]$ \DisplayProof \\[4ex] \Axiom$ !A(a), \Gamma \fCenter \Delta $ \RightLabel{\LeftR{\lexists}} \UnaryInf$ \lexists[x][!A(x)], \Gamma \fCenter \Delta$ \DisplayProof & \Axiom$ \Gamma \fCenter !A(t) $ \RightLabel{\RightR{\lexists}} \UnaryInf$ \Gamma \fCenter \lexists[x][!A(x)]$ \DisplayProof \end{tabular} \caption{Rules of \Log{G3i} for intuitionistic logic. In $\RightR{\forall}$ and $\LeftR{\exists}$, the !!{constant}~$a$ must not occur in the conclusion sequent. $\Gamma$ is a multisets of !!{formula}s, and $\Delta$ may be empty or contain a single !!{formula}. In axioms, the !!{formula}~$!C$ must be atomic. \Log{G1m} is \Log{G1i} without axioms $\lfalse, \Gamma \Sequent \Delta$.} \ollabel{tab:G3i} \end{table} \end{document}

Referencing norms: G3I

en · official · sha256:04fc54bec445b78a7c47a7c9db8a8fbb38feb33fc693a90bd530238d118cd485

% Part: proof-theory % Chapter: sequent-calculus % Section: rules-LK \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \begin{table} \begin{tabular}{@{}c@{}c@{}} \multicolumn{2}{@{}c@{}}{Axioms}\\[2ex] $!A \Sequent !A$ & $\lfalse \Sequent \quad$ \\[2ex] \multicolumn{2}{@{}c@{}}{Structural Rules}\\[2ex] \Axiom$ \Gamma \fCenter \Delta $ \RightLabel{\LeftR{\Weakening}} \UnaryInf$ !A, \Gamma \fCenter \Delta$ \DisplayProof & \Axiom$ \Gamma \fCenter \Delta$ \RightLabel{\RightR{\Weakening}} \UnaryInf$ \Gamma \fCenter \Delta, !A$ \DisplayProof \\[4ex] \Axiom$ !A, !A, \Gamma \fCenter \Delta $ \RightLabel{\LeftR{\Contraction}} \UnaryInf$ !A, \Gamma \fCenter \Delta$ \DisplayProof & \Axiom$ \Gamma \fCenter \Delta, !A, !A$ \RightLabel{\RightR{\Contraction}} \UnaryInf$ \Gamma \fCenter \Delta, !A$ \DisplayProof \\[4ex] \Axiom$ \Gamma, !A, !B, \Pi \fCenter \Delta $ \RightLabel{\LeftR{\Exchange}} \UnaryInf$\Gamma, !B, !A, \Pi \fCenter \Delta$ \DisplayProof & \Axiom$ \Gamma \fCenter \Delta, !A, !B, \Lambda$ \RightLabel{\RightR{\Exchange}} \UnaryInf$ \Gamma \fCenter \Delta, !B, !A, \Lambda$ \DisplayProof \\[4ex] \multicolumn{2}{@{}c@{}}{Logical Rules}\\[2ex] \Axiom$ \Gamma \fCenter \Delta, !A $ \RightLabel{\LeftR{\lnot}} \UnaryInf$ \lnot !A, \Gamma \fCenter \Delta$ \DisplayProof & \Axiom$!A, \Gamma \fCenter \Delta$ \RightLabel{\RightR{\lnot}} \UnaryInf$ \Gamma \fCenter \Delta, \lnot !A $ \DisplayProof \\[4ex]\begin{tabular}[t]{@{}l@{}} \Axiom$ !A, \Gamma \fCenter \Delta$ \RightLabel{\LeftR{\land}} \UnaryInf$ !A \land !B, \Gamma \fCenter \Delta$ \DisplayProof \\[3ex] \Axiom$!B, \Gamma \fCenter \Delta$ \RightLabel{\LeftR{\land}} \UnaryInf$!A \land !B, \Gamma \fCenter \Delta$ \DisplayProof\\[3ex] \end{tabular} & \Axiom$\Gamma \fCenter \Delta, !A$ \Axiom$ \Gamma \fCenter \Delta, !B$ \RightLabel{\RightR{\land}} \BinaryInf$ \Gamma \fCenter \Delta, !A \land !B $ \DisplayProof \\[4ex]\Axiom$!A, \Gamma \fCenter \Delta$ \Axiom$!B, \Gamma \fCenter \Delta$ \RightLabel{\LeftR{\lor}} \BinaryInf$!A \lor !B, \Gamma \fCenter \Delta$ \DisplayProof & \begin{tabular}[t]{@{}r@{}} \Axiom$\Gamma \fCenter \Delta, !A$ \RightLabel{\RightR{\lor}} \UnaryInf$ \Gamma \fCenter \Delta, !A \lor !B$ \DisplayProof \\[3ex] \Axiom$ \Gamma \fCenter \Delta, !B$ \RightLabel{\RightR{\lor}} \UnaryInf$ \Gamma \fCenter \Delta, !A \lor !B$ \DisplayProof\\[3ex] \end{tabular} \\[4ex] \Axiom$ \Gamma \fCenter \Delta, !A$ \Axiom$ !B, \Gamma \fCenter \Delta$ \RightLabel{\LeftR{\lif}} \BinaryInf$ !A \lif !B, \Gamma \fCenter \Delta$ \DisplayProof & \Axiom$ !A, \Gamma \fCenter \Delta, !B$ \RightLabel{\RightR{\lif}} \UnaryInf$ \Gamma \fCenter \Delta, !A \lif !B $ \DisplayProof \\[4ex] \Axiom$ !A(t), \Gamma \fCenter \Delta$ \RightLabel{\LeftR{\lforall}} \UnaryInf$ \lforall[x][!A(x)],\Gamma \fCenter \Delta$ \DisplayProof & \Axiom$ \Gamma \fCenter \Delta, !A(a) $ \RightLabel{\RightR{\lforall}} \UnaryInf$ \Gamma \fCenter \Delta, \lforall[x][!A(x)]$ \DisplayProof \\[4ex] \Axiom$ !A(a), \Gamma \fCenter \Delta $ \RightLabel{\LeftR{\lexists}} \UnaryInf$ \lexists[x][!A(x)], \Gamma \fCenter \Delta$ \DisplayProof & \Axiom$ \Gamma \fCenter \Delta, !A(t) $ \RightLabel{\RightR{\lexists}} \UnaryInf$ \Gamma \fCenter \Delta, \lexists[x][!A(x)]$ \DisplayProof \end{tabular} \caption{Rules of \Log{LK}. In $\RightR{\forall}$ and $\LeftR{\exists}$, the !!{constant}~$a$ must not occur in the conclusion sequent. $\Gamma$, $\Delta$, and~$\Pi$ are sequences of !!{formula}s.} \ollabel{tab:G1c} \end{table} \end{document}

Referencing norms: LK, LK_ALL_R, LK_AXIOM, LK_IF_L, LK_IF_R, LK_NOT_R, LK_WEAKENING_R, SEQUENT, S_LKIFL_C, S_LKIFL_CA, S_LKIFL_CB, S_LKIFL_CIMP, S_LKIFL_P1, S_LKIFL_P2, V_LKIFL_A, V_LKIFL_B