The Open Logic Text

en · official · sha256:8b431994a9e3c59f8970b145b81467b95f8cf483e81ed787132f565c5add799dEN

% Part: first-order-logic % Chapter: beyond % Section: intuitionistic-logic \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{byd}{il} \olsection{Intuitionistic Logic} In contrast to second-order and higher-order logic, intuitionistic first-order logic represents a restriction of the classical version, intended to model a more ``constructive'' kind of reasoning. The following examples may serve to illustrate some of the underlying motivations. Suppose someone came up to you one day and announced that they had determined a natural number~$x$, with the property that if $x$ is prime, the Riemann hypothesis is true, and if $x$ is composite, the Riemann hypothesis is false. Great news!{} Whether the Riemann hypothesis is true or not is one of the big open questions of mathematics, and here they seem to have reduced the problem to one of calculation, that is, to the determination of whether a specific number is prime or not. What is the magic value of $x$? They describe it as follows: $x$ is the natural number that is equal to $7$ if the Riemann hypothesis is true, and $9$ otherwise. Angrily, you demand your money back. From a classical point of view, the description above does in fact determine a unique value of $x$; but what you really want is a value of $x$ that is given \emph{explicitly}. To take another, perhaps less contrived example, consider the following question. We know that it is possible to raise an irrational number to a rational power, and get a rational result. For example, $\sqrt{2}^2 = 2$. What is less clear is whether or not it is possible to raise an irrational number to an \emph{irrational} power, and get a rational result. The following theorem answers this in the affirmative: \begin{thm} There are irrational numbers $a$ and $b$ such that $a^b$ is rational. \end{thm} \begin{proof} Consider $\sqrt{2}^{\sqrt{2}}$. If this is rational, we are done: we can let $a = b = \sqrt{2}$. Otherwise, it is irrational. Then we have \[ (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^{\sqrt{2} \cdot \sqrt{2}} = \sqrt{2}^2 = 2, \] which is certainly rational. So, in this case, let $a$ be $\sqrt{2}^{\sqrt{2}}$, and let $b$ be~$\sqrt 2$. \end{proof} Does this constitute a valid proof? Most mathematicians feel that it does. But again, there is something a little bit unsatisfying here: we have proved the existence of a pair of real numbers with a certain property, without being able to say \emph{which} pair of numbers it is. It is possible to prove the same result, but in such a way that the pair $a$, $b$ \emph{is} given in the proof: take $a = \sqrt{3}$ and $b = \log_3 4$. Then \[ a^b = \sqrt{3}^{\log_3 4} = 3^{1/2 \cdot \log_3 4} = (3^{\log_3 4})^{1/2} = 4^{1/2}= 2, \] since $3^{\log_3 x} = x$. Intuitionistic logic is designed to model a kind of reasoning where moves like the one in the first proof are disallowed. Proving the existence of an $x$ satisfying~$!A(x)$ means that you have to give a specific~$x$, and a proof that it satisfies $!A$, like in the second proof. Proving that $!A$ or $!B$ holds requires that you can prove one or the other. Formally speaking, intuitionistic first-order logic is what you get if you restrict !!a{derivation} system for first-order logic in a certain way. Similarly, there are intuitionistic versions of second-order or higher-order logic. From the mathematical point of view, these are just formal deductive systems, but, as already noted, they are intended to model a kind of mathematical reasoning. One can take this to be the kind of reasoning that is justified on a certain philosophical view of mathematics (such as Brouwer's intuitionism); one can take it to be a kind of mathematical reasoning which is more ``concrete'' and satisfying (along the lines of Bishop's constructivism); and one can argue about whether or not the formal description captures the informal motivation. But whatever philosophical positions we may hold, we can study intuitionistic logic as a formally presented logic; and for whatever reasons, many mathematical logicians find it interesting to do so. There is an informal constructive interpretation of the intuitionist connectives, usually known as the BHK interpretation (named after Brouwer, Heyting, and Kolmogorov). It runs as follows: a proof of $!A \land !B$ consists of a proof of $!A$ paired with a proof of $!B$; a proof of $!A \lor !B$ consists of either a proof of $!A$, or a proof of $!B$, where we have explicit information as to which is the case; a proof of $!A \lif !B$ consists of a procedure, which transforms a proof of $!A$ to a proof of~$!B$; a proof of $\lforall[x][!A(x)]$ consists of a procedure which returns a proof of $!A(x)$ for any value of~$x$; and a proof of $\lexists[x][!A(x)]$ consists of a value of~$x$, together with a proof that this value satisfies~$!A$. One can describe the interpretation in computational terms known as the ``Curry--Howard isomorphism'' or the ``!!{formula}s-as-types paradigm'': think of !!a{formula} as specifying a certain kind of data type, and proofs as computational objects of these data types that enable us to see that the corresponding !!{formula} is true. Intuitionistic logic is often thought of as being classical logic ``minus'' the law of the excluded middle. This following theorem makes this more precise. \begin{thm} Intuitionistically, the following axiom schemata are equivalent: \begin{enumerate} \item $(\lnot !A \lif \lfalse) \lif !A$. \item $!A \lor \lnot !A$ \item $\lnot \lnot !A \lif !A$ \end{enumerate} \end{thm} Obtaining instances of one schema from either of the others is a good exercise in intuitionistic logic. The first deductive systems for intuitionistic propositional logic, put forth as formalizations of Brouwer's intuitionism, are due, independently, to Kolmogorov, Glivenko, and Heyting. The first formalization of intuitionistic first-order logic (and parts of intuitionist mathematics) is due to Heyting. Though a number of classically valid schemata are not intuitionistically valid, many are. The \emph{double-negation translation} describes an important relationship between classical and intuitionist logic. It is defined inductively follows (think of $!A^N$ as the ``intuitionist'' translation of the classical !!{formula}~$!A$): \begin{align*} !A^N & \ident \lnot\lnot !A \quad \text{for atomic !!{formula}s $!A$} \\ (!A \land !B)^N & \ident (!A^N \land !B^N) \\ (!A \lor !B)^N & \ident \lnot\lnot (!A^N \lor !B^N) \\ (!A \lif !B)^N & \ident (!A^N \lif !B^N) \\ (\lforall[x][!A])^N & \ident \lforall[x][!A^N] \\ (\lexists[x][!A])^N & \ident \lnot\lnot\lexists[x][!A^N] \end{align*} Kolmogorov and Glivenko had versions of this translation for propositional logic; for predicate logic, it is due to G\"odel and Gentzen, independently. We have \begin{thm} \begin{enumerate} \item $!A \liff !A^N$ is provable classically \item If $!A$ is provable classically, then $!A^N$ is provable intuitionistically. \end{enumerate} \end{thm} We can now envision the following dialogue. Classical mathematician: ``I've proved $!A$!'' Intuitionist mathematician: ``Your proof isn't valid. What you've really proved is $!A^N$.'' Classical mathematician: ``Fine by me!'' As far as the classical mathematician is concerned, the intuitionist is just splitting hairs, since the two are equivalent. But the intuitionist insists there is a difference. Note that the above translation concerns pure logic only; it does not address the question as to what the appropriate \emph{nonlogical} axioms are for classical and intuitionistic mathematics, or what the relationship is between them. But the following slight extension of the theorem above provides some useful information: \begin{thm} If $\Gamma$ proves $!A$ classically, $\Gamma^N$ proves $!A^N$ intuitionistically. \end{thm} In other words, if $!A$ is provable from some hypotheses classically, then $!A^N$ is provable from their double-negation translations. To show that a sentence or propositional !!{formula} is intuitionistically valid, all you have to do is provide a proof. But how can you show that it is not valid? For that purpose, we need a semantics that is sound, and preferably complete. A semantics due to Kripke nicely fits the bill. We can play the same game we did for classical logic: define the semantics, and prove soundness and completeness. It is worthwhile, however, to note the following distinction. In the case of classical logic, the semantics was the ``obvious'' one, in a sense implicit in the meaning of the connectives. Though one can provide some intuitive motivation for Kripke semantics, the latter does not offer the same feeling of inevitability. In addition, the notion of a classical !!{structure} is a natural mathematical one, so we can either take the notion of !!a{structure} to be a tool for studying classical first-order logic, or take classical first-order logic to be a tool for studying mathematical !!{structure}s. In contrast, Kripke !!{structure}s can only be viewed as a logical construct; they don't seem to have independent mathematical interest. A Kripke !!{structure}~$\mModel M = \tuple{W, R, V}$ for a propositional language consists of a set~$W$, partial order~$R$ on~$W$ with a least !!{element}, and an ``monotone'' assignment of propositional variables to the !!{element}s of~$W$. The intuition is that the !!{element}s of $W$ represent ``worlds,'' or ``states of knowledge''; an element $v \geq u$ represents a ``possible future state'' of~$u$; and the propositional variables assigned to~$u$ are the propositions that are known to be true in state~$u$. The forcing relation $\mSat{M}{!A}[w]$ then extends this relationship to arbitrary !!{formula}s in the language; read $\mSat{M}{!A}[w]$ as ``$!A$ is true in state~$w$.'' The relationship is defined inductively, as follows: \begin{enumerate} \item $\mSat{M}{\Obj p_i}[w]$ iff $\Obj p_i$ is one of the propositional variables assigned to~$w$. \item $\mSat/{M}{\lfalse}[w]$. \item $\mSat{M}{(!A \land !B)}[w]$ iff $\mSat{M}{!A}[w]$ and $\mSat{M}{!B}[w]$. \item $\mSat{M}{(!A \lor !B)}[w]$ iff $\mSat{M}{!A}[w]$ or $\mSat{M}{!B}[w]$. \item $\mSat{M}{(!A \lif !B)}[w]$ iff, whenever $w' \geq w$ and $\mSat{M}{!A}[w']$, then $\mSat{M}{!B}[w']$. \end{enumerate} It is a good exercise to try to show that $\lnot (p \land q) \lif (\lnot p \lor \lnot q)$ is not intuitionistically valid, by cooking up a Kripke !!{structure} that provides a counterexample. \end{document}

Ссылаются нормы: P_DOUBLE_NEGATION, P_EXCLUDED_MIDDLE, P_REDUCTIO_SCHEMA, S_LEM, S_LEM_L, S_LEM_R, S_LEM_RA, V_LEM_A

en · official · sha256:0ec2ba4bbefb8b782b0f375b04244a5bb34ae2b45378bbdcbb8bee93622c9462EN

% Part: first-order-logic % Chapter: completeness % Section: identity \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{com}{ide} \olsection{Identity} \begin{explain} The construction of the term model given in the preceding section is enough to establish completeness for first-order logic for sets~$\Gamma$ that do not contain~$\eq$. The term model satisfies every $!A \in \Gamma^*$ which does not contain~$\eq$ (and hence all $!A \in \Gamma$). It does not work, however, if $\eq$ is present. The reason is that $\Gamma^*$ then may contain !!a{sentence}~$\eq[t][t']$, but in the term model the value of any term is that term itself. Hence, if $t$ and $t'$ are different terms, their values in the term model---i.e., $t$ and $t'$, respectively---are different, and so $\eq[t][t']$ is false. We can fix this, however, using a construction known as ``factoring.'' \end{explain} \begin{defn} Let $\Gamma^*$ be a consistent and !!{complete} set of sentences in~$\Lang L$. We define the relation $\approx$ on the set of closed terms of~$\Lang L$ by \[ t \approx t' \text{\quad iff \quad} \eq[t][t'] \in \Gamma^* \] \end{defn} \begin{prop} \ollabel{prop:approx-equiv} The relation $\approx$ has the following properties: \begin{enumerate} \item $\approx$ is reflexive. \item $\approx$ is symmetric. \item $\approx$ is transitive. \item If $t \approx t'$, $f$ is !!a{function}, and $t_1$, \dots, $t_{i-1}$, $t_{i+1}$, \dots, $t_n$ are closed terms, then \[ \Atom{f}{t_1,\dots, t_{i-1}, t, t_{i+1}, \dots, t_n} \approx \Atom{f}{t_1,\dots, t_{i-1}, t', t_{i+1}, \dots, t_n}. \] \item If $t \approx t'$, $R$ is !!a{predicate}, and $t_1$, \dots, $t_{i-1}$, $t_{i+1}$, \dots, $t_n$ are closed terms, then \begin{multline*} \Atom{R}{t_1,\dots, t_{i-1}, t, t_{i+1}, \dots, t_n} \in \Gamma^* \text{ iff } \\ \Atom{R}{t_1,\dots, t_{i-1}, t', t_{i+1}, \dots, t_n} \in \Gamma^*. \end{multline*} \end{enumerate} \end{prop} \begin{proof} Since $\Gamma^*$ is consistent and !!{complete}, $\eq[t][t'] \in \Gamma^*$ iff $\Gamma^* \Proves \eq[t][t']$. Thus it is enough to show the following: \begin{enumerate} \item $\Gamma^* \Proves \eq[t][t]$ for all closed terms~$t$. \item If $\Gamma^* \Proves \eq[t][t']$ then $\Gamma^* \Proves \eq[t'][t]$. \item If $\Gamma^* \Proves \eq[t][t']$ and $\Gamma^* \Proves \eq[t'][t'']$, then $\Gamma^* \Proves \eq[t][t'']$. \item If $\Gamma^* \Proves \eq[t][t']$, then \[ \Gamma^* \Proves \eq[\Atom{f}{t_1,\dots,t_{i-1},t,t_{i+1},,\dots,t_n}][\Atom{f}{t_1,\dots,t_{i-1},t',t_{i+1},\dots,t_n}] \] for every $n$-place !!{function}~$f$ and closed terms $t_1$, \dots, $t_{i-1}$, $t_{i+1}$, \dots,~$t_n$. \item If $\Gamma^* \Proves \eq[t][t']$ and $\Gamma^* \Proves \Atom{R}{t_1,\dots,t_{i-1},t,t_{i+1},\dots,t_n}$, then $\Gamma^* \Proves \Atom{R}{t_1,\dots,t_{i-1},t',t_{i+1},\dots,t_n}$ for every $n$-place !!{predicate}~$R$ and closed terms $t_1$, \dots, $t_{i-1}$, $t_{i+1}$, \dots,~$t_n$. \end{enumerate} \end{proof} \begin{prob} Complete the proof of~\olref[fol][com][ide]{prop:approx-equiv}. \end{prob} \begin{defn} Suppose $\Gamma^*$ is a consistent and !!{complete} set in a language~$\Lang L$, $t$ is a closed term, and $\approx$ as in the previous definition. Then: \[ \equivrep{t}{\approx} = \Setabs{t'}{t'\in \Trm[L], t \approx t'} \] and $\equivclass{\Trm[L]}{\approx} = \Setabs{\equivrep{t}{\approx}}{t \in \Trm[L]}$. \end{defn} \begin{defn} \ollabel{defn:term-model-factor} Let $\Struct M = \Struct M(\Gamma^*)$ be the term model for~$\Gamma^*$ from \olref[mod]{defn:termmodel}. Then $\Struct{\equivclass{M}{\approx}}$ is the following !!{structure}: \begin{enumerate} \item $\Domain{\equivclass{M}{\approx}} = \equivclass{\Trm[L]}{\approx}$. \item $\Assign{c}{\equivclass{M}{\approx}} = \equivrep{c}{\approx}$ \item $\Assign{f}{\equivclass{M}{\approx}}(\equivrep{t_1}{\approx}, \dots, \equivrep{t_n}{\approx}) = \equivrep{\Atom{f}{t_1,\dots, t_n}}{\approx}$ \item $\tuple{\equivrep{t_1}{\approx}, \dots, \equivrep{t_n}{\approx}} \in \Assign{R}{\equivclass{M}{\approx}}$ iff $\Sat{M}{\Atom{R}{t_1,\dots, t_n}}$, i.e., iff $\Atom{R}{t_1,\dots, t_n} \in \Gamma^*$. \end{enumerate} \end{defn} \begin{explain} Note that we have defined $\Assign{f}{\equivclass{M}{\approx}}$ and $\Assign{R}{\equivclass{M}{\approx}}$ for elements of $\equivclass{\Trm[L]}{\approx}$ by referring to them as $\equivrep{t}{\approx}$, i.e., via \emph{representatives}~$t \in \equivrep{t}{\approx}$. We have to make sure that these definitions do not depend on the choice of these representatives, i.e., that for some other choices~$t'$ which determine the same equivalence classes ($\equivrep{t}{\approx} = \equivrep{t'}{\approx}$), the definitions yield the same result. For instance, if $R$ is a one-place !!{predicate}, the last clause of the definition says that $\equivrep{t}{\approx} \in \Assign{R}{\equivclass{M}{\approx}}$ iff $\Sat{M}{\Atom{R}{t}}$. If for some other term~$t'$ with $t \approx t'$, $\Sat/{M}{\Atom{R}{t}}$, then the definition would require $\equivrep{t'}{\approx} \notin \Assign{R}{\equivclass{M}{\approx}}$. If $t \approx t'$, then $\equivrep{t}{\approx} = \equivrep{t'}{\approx}$, but we can't have both $\equivrep{t}{\approx} \in \Assign{R}{\equivclass{M}{\approx}}$ and $\equivrep{t}{\approx} \notin \Assign{R}{\equivclass{M}{\approx}}$. However, \olref{prop:approx-equiv} guarantees that this cannot happen. \end{explain} \begin{prop} $\Struct{\equivclass{M}{\approx}}$ is well defined, i.e., if $t_1$, \dots, $t_n$, $t_1'$, \dots, $t_n'$ are closed terms, and $t_i \approx t_i'$ then \begin{enumerate} \item $\equivrep{\Atom{f}{t_1,\dots, t_n}}{\approx} = \equivrep{\Atom{f}{t_1',\dots, t_n'}}{\approx}$, i.e., \[ \Atom{f}{t_1,\dots, t_n} \approx \Atom{f}{t_1',\dots, t_n'} \] and \item $\Sat{M}{\Atom{R}{t_1,\dots, t_n}}$ iff $\Sat{M}{\Atom{R}{t_1',\dots, t_n'}}$, i.e., \[ \Atom{R}{t_1,\dots, t_n} \in \Gamma^* \text{ iff } \Atom{R}{t_1',\dots, t_n'} \in \Gamma^*. \] \end{enumerate} \end{prop} \begin{proof} Follows from \olref{prop:approx-equiv} by induction on~$n$. \end{proof} As in the case of the term model, before proving the truth lemma we need the following lemma. \begin{lem} \ollabel{lem:val-in-termmodel-factored} Let $\Struct M = \Struct M (\Gamma^*)$, then $\Value{t}{\equivclass{M}{\approx}} = \equivrep{t} {\approx}$. \end{lem} \begin{proof} The proof is similar to that of \olref[mod]{lem:val-in-termmodel}. \end{proof} \begin{prob} Complete the proof of~\olref[fol][com][ide]{lem:val-in-termmodel-factored}. \end{prob} \begin{lem} \ollabel{lem:truth} $\Sat{\equivclass{M}{\approx}}{!A}$ iff $!A \in \Gamma^*$ for all sentences~$!A$. \end{lem} \begin{proof} By induction on~$!A$, just as in the proof of \olref[mod]{lem:truth}. The only case that needs additional attention is when $!A \ident \eq[t][t']$. \begin{align*} \Sat{\equivclass{M}{\approx}}{\eq[t][t']} & \text{ iff } \equivrep{t}{\approx} = \equivrep{t'}{\approx} \text{ (by definition of $\Struct{\equivclass{M}{\approx}}$)}\\ & \text{ iff } t \approx t' \text{ (by definition of $\equivrep{t}{\approx}$)}\\ & \text{ iff } \eq[t][t'] \in \Gamma^* \text{ (by definition of $\approx$).} \end{align*} \end{proof} \begin{digress} Note that while $\Struct{M(\Gamma^*)}$ is always !!{enumerable} and infinite, $\Struct{\equivclass{M}{\approx}}$ may be finite, since it may turn out that there are only finitely many classes $\equivrep{t}{\approx}$. This is to be expected, since $\Gamma$ may contain !!{sentence}s which require any !!{structure} in which they are true to be finite. For instance, $\lforall[x][\lforall[y][x = y]]$ is a consistent !!{sentence}, but is satisfied only in !!{structure}s with !!a{domain} that contains exactly one !!{element}. \end{digress} \end{document}

en · official · sha256:2b7f445305e77d9971ced53cd2db81d2f3f7c07f0099151f1e14a198043d11aeEN

% Part: first-order-logic % Chapter: natural-deduction % Section: identity \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{ntd}{ide} \olsection{\usetoken{P}{derivation} with \usetoken{S}{identity}} !!^{derivation}s with !!{identity} require additional inference rules. \begin{defish} \AxiomC{} \RightLabel{\Intro{\eq}} \UnaryInfC{$\eq[t][t]$} \DisplayProof \hfill \begin{tabular}{r} \AxiomC{$\eq[t_1][t_2]$} \AxiomC{$!A(t_1)$} \RightLabel{\Elim{\eq}} \BinaryInfC{$!A(t_2)$} \DisplayProof \\[3ex] \AxiomC{$\eq[t_1][t_2]$} \AxiomC{$!A(t_2)$} \RightLabel{\Elim{\eq}} \BinaryInfC{$!A(t_1)$} \DisplayProof \end{tabular} \end{defish} In the above rules, $t$, $t_1$, and $t_2$ are closed terms. The \Intro{\eq} rule allows us to !!{derive} any identity statement of the form $\eq[t][t]$ outright, from no assumptions. \begin{ex} If $s$ and $t$ are closed terms, then $!A(s), \eq[s][t] \Proves !A(t)$: \begin{prooftree} \AxiomC{$\eq[s][t]$} \AxiomC{$!A(s)$} \RightLabel{$\Elim{\eq}$} \BinaryInfC{$!A(t)$} \end{prooftree} This may be familiar as the ``principle of substitutability of identicals,'' or Leibniz' Law. \end{ex} \begin{prob} Prove that $=$ is both symmetric and transitive, i.e., give !!{derivation}s of $\lforall[x][\lforall[y][(\eq[x][y] \lif \eq[y][x])]]$ and $\lforall[x][\lforall[y][\lforall[z]((\eq[x][y] \land \eq[y][z]) \lif \eq[x][z])]]$ \end{prob} \begin{ex} We !!{derive} the !!{sentence} \begin{align*} & \lforall[x][\lforall[y][((!A(x) \land !A(y)) \lif \eq[x][y])]] \intertext{from the !!{sentence}} & \lexists[x][\lforall[y][(!A(y) \lif \eq[y][x])]] \end{align*} We develop the !!{derivation} backwards: \begin{prooftree} \AxiomC{$\lexists[x][\lforall[y][(!A(y) \lif \eq[y][x])]] \quad \Discharge{!A(a) \land !A(b)}{1}$} \DeduceC{$\eq[a][b]$} \DischargeRule{\Intro{\lif}}{1} \UnaryInfC{$((!A(a) \land !A(b)) \lif \eq[a][b])$} \RightLabel{\Intro{\lforall}} \UnaryInfC{$\lforall[y][((!A(a) \land !A(y)) \lif \eq[a][y])]$} \RightLabel{\Intro{\lforall}} \UnaryInfC{$\lforall[x][\lforall[y][((!A(x) \land !A(y)) \lif \eq[x][y])]]$} \end{prooftree} We'll now have to use the main assumption: since it is an existential !!{formula}, we use \Elim{\lexists} to !!{derive} the intermediary conclusion $\eq[a][b]$. \begin{prooftree} \AxiomC{$\lexists[x][\lforall[y][(!A(y) \lif \eq[y][x])]]$} \AxiomC{$\Discharge{\lforall[y][(!A(y) \lif \eq[y][c]])}{2}$} \noLine \UnaryInfC{$\Discharge{!A(a) \land !A(b)}{1}$} \DeduceC{$\eq[a][b]$} \DischargeRule{\Elim{\lexists}}{2} \BinaryInfC{$\eq[a][b]$} \DischargeRule{\Intro{\lif}}{1} \UnaryInfC{$((!A(a) \land !A(b)) \lif \eq[a][b])$} \RightLabel{\Intro{\lforall}} \UnaryInfC{$\lforall[y][((!A(a) \land !A(y)) \lif \eq[a][y])]$} \RightLabel{\Intro{\lforall}} \UnaryInfC{$\lforall[x][\lforall[y][((!A(x) \land !A(y)) \lif \eq[x][y])]]$} \end{prooftree} The sub-!!{derivation} on the top right is completed by using its assumptions to show that $\eq[a][c]$ and $\eq[b][c]$. This requires two separate !!{derivation}s. The !!{derivation} for $\eq[a][c]$ is as follows: \begin{prooftree} \AxiomC{$\Discharge{\lforall[y][(!A(y) \lif \eq[y][c]])}{2}$} \RightLabel{\Elim{\lforall}} \UnaryInfC{$!A(a) \lif \eq[a][c]$} \AxiomC{$\Discharge{!A(a) \land !A(b)}{1}$} \RightLabel{\Elim{\land}} \UnaryInfC{$!A(a)$} \RightLabel{\Elim{\lif}} \BinaryInfC{$\eq[a][c]$} \end{prooftree} From $\eq[a][c]$ and $\eq[b][c]$ we !!{derive} $\eq[a][b]$ by \Elim{\eq}. \end{ex} \begin{prob} Give !!{derivation}s of the following !!{formula}s: \begin{enumerate} \item $\lforall[x][\lforall[y][((\eq[x][y] \land !A(x)) \lif !A(y))]]$ \item $\lexists[x][!A(x)] \land \lforall[y][\lforall[z][((!A(y) \land !A(z)) \lif \eq[y][z])]] \lif \lexists[x][(!A(x) \land \lforall[y][(!A(y) \lif \eq[y][x])])]$ \end{enumerate} \end{prob} \end{document}

Ссылаются нормы: EQ_ELIM, EQ_INTRO, S_EQE_C, S_EQE_CA, S_EQE_P1, S_EQE_P2, S_EQE_P2A, S_EQI_C, V_EQE_A

en · official · sha256:547c899165a35871c54e903df7ee2848890b405e96d09fab14dbb7718d720c13EN

% Part: first-order-logic % Chapter: syntax-and-semantics % Section: introduction \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{syn}{int} \olsection{Introduction} In order to develop the theory and metatheory of first-order logic, we must first define the syntax and semantics of its expressions. The expressions of first-order logic are terms and !!{formula}s. Terms are formed from !!{variable}s, !!{constant}s, and !!{function}s. !!^{formula}s, in turn, are formed from !!{predicate}s together with terms (these form the smallest, ``atomic'' !!{formula}s), and then from atomic !!{formula}s we can form more complex ones using logical connectives and quantifiers. There are many different ways to set down the formation rules; we give just one possible one. Other systems will chose different symbols, will select different sets of connectives as primitive, will use parentheses differently (or even not at all, as in the case of so-called Polish notation). What all approaches have in common, though, is that the formation rules define the set of terms and !!{formula}s \emph{inductively}. If done properly, every expression can result essentially in only one way according to the formation rules. The inductive definition resulting in expressions that are \emph{uniquely readable} means we can give meanings to these expressions using the same method---inductive definition. Giving the meaning of expressions is the domain of semantics. The central concept in semantics is that of satisfaction in !!a{structure}. !!^a{structure} gives meaning to the building blocks of the language: !!a{domain} is a non-empty set of objects. The quantifiers are interpreted as ranging over this domain, !!{constant}s are assigned elements in the domain, !!{function}s are assigned functions from the !!{domain} to itself, and !!{predicate}s are assigned relations on the !!{domain}. The !!{domain} together with assignments to the basic vocabulary constitutes !!a{structure}. !!^{variable}s may appear in !!{formula}s, and in order to give a semantics, we also have to assign !!{element}s of the !!{domain} to them---this is a variable assignment. The satisfaction relation, finally, brings these together. !!^a{formula} may be satisfied in !!a{structure}~$\Struct{M}$ relative to a variable assignment~$s$, written as $\Sat{M}{!A}[s]$. This relation is also defined by induction on the structure of~$!A$, using the truth tables for the logical connectives to define, say, satisfaction of $!A \land !B$ in terms of satisfaction (or not) of $!A$ and ~$!B$. It then turns out that the variable assignment is irrelevant if the !!{formula}~$!A$ is !!a{sentence}, i.e., has no free variables, and so we can talk of !!{sentence}s being simply satisfied (or not) in !!{structure}s. On the basis of the satisfaction relation $\Sat{M}{!A}$ for sentences we can then define the basic semantic notions of validity, entailment, and satisfiability. A sentence is valid, $\Entails !A$, if every structure satisfies it. It is entailed by a set of !!{sentence}s, $\Gamma \Entails !A$, if every !!{structure} that satisfies all the !!{sentence}s in~$\Gamma$ also satisfies~$!A$. And a set of sentences is satisfiable if some !!{structure} satisfies all !!{sentence}s in it at the same time. Because !!{formula}s are inductively defined, and satisfaction is in turn defined by induction on the structure of !!{formula}s, we can use induction to prove properties of our semantics and to relate the semantic notions defined. \end{document}

Ссылаются нормы: CFOL, IdentitySettled, identity_is_settled, identity_treatment

en · official · sha256:41127c788b9c4f683c1ec00a35ad1fcc42fb180e3c0326d799cea2072dae3f8eEN

% Part: propositional-logic % Chapter: syntax-and-semantics % Section: introduction \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{pl}{syn}{int} \olsection{Introduction} Propositional logic deals with !!{formula}s that are built from !!{propositional variable}s using the propositional connectives $\lnot$, $\land$, $\lor$, $\lif$, and $\liff$. Intuitively, !!a{propositional variable}~$p$ stands for a sentence or proposition that is true or false. Whenever the ``truth value'' of the !!{propositional variable} in !!a{formula} is determined, so is the truth value of any !!{formula}s formed from them using propositional connectives. We say that propositional logic is \emph{truth functional}, because its semantics is given by functions of truth values. In particular, in propositional logic we leave out of consideration any further determination of truth and falsity, e.g., whether something is necessarily true rather than just contingently true, or whether something is known to be true, or whether something is true now rather than was true or will be true. We only consider two truth values true ($\True$) and false ($\False$), and so exclude from discussion the possibility that a statement may be neither true nor false, or only half true. We also concentrate only on connectives where the truth value of !!a{formula} built from them is completely determined by the truth values of its parts (and not, say, on its meaning). In particular, whether the truth value of conditionals in English is truth functional in this sense is contentious. The material conditional~$\lif$ is; other logics deal with conditionals that are not truth functional. In order to develop the theory and metatheory of truth-functional propositional logic, we must first define the syntax and semantics of its expressions. We will describe one way of constructing !!{formula}s from !!{propositional variable}s using the connectives. Alternative definitions are possible. Other systems will choose different symbols, will select different sets of connectives as primitive, and will use parentheses differently (or even not at all, as in the case of so-called Polish notation). What all approaches have in common, though, is that the formation rules define the set of !!{formula}s \emph{inductively}. If done properly, every expression can result essentially in only one way according to the formation rules. The inductive definition resulting in expressions that are \emph{uniquely readable} means we can give meanings to these expressions using the same method---inductive definition. Giving the meaning of expressions is the domain of semantics. The central concept in semantics for propositional logic is that of satisfaction in !!a{valuation}. !!^a{valuation}~$\pAssign{v}$ assigns truth values $\True$, $\False$ to the !!{propositional variable}s. Any !!{valuation} determines a truth value $\pValue{v}(!A)$ for any !!{formula}~$!A$. !!^a{formula} is satisfied in !!a{valuation}~$\pAssign{v}$ iff $\pValue{v}(!A) = \True$---we write this as $\pSat{v}{!A}$. This relation can also be defined by induction on the structure of~$!A$, using the truth functions for the logical connectives to define, say, satisfaction of $!A \land !B$ in terms of satisfaction (or not) of $!A$ and~$!B$. On the basis of the satisfaction relation $\pSat{v}{!A}$ for sentences we can then define the basic semantic notions of tautology, entailment, and satisfiability. !!^a{formula} is a tautology, $\Entails !A$, if every !!{valuation} satisfies it, i.e., $\pValue{v}(!A) = \True$ for any~$\pAssign{v}$. It is entailed by a set of !!{formula}s, $\Gamma \Entails !A$, if every !!{valuation} that satisfies all the !!{formula}s in~$\Gamma$ also satisfies~$!A$. And a set of !!{formula}s is satisfiable if some !!{valuation} satisfies all !!{formula}s in it at the same time. Because !!{formula}s are inductively defined, and satisfaction is in turn defined by induction on the structure of !!{formula}s, we can use induction to prove properties of our semantics and to relate the semantic notions defined. \end{document}

Ссылаются нормы: CPL, P_BIVALENCE, P_TRUTH_FUNCTIONALITY