mirror of
https://github.com/ganelson/inform.git
synced 2024-07-17 06:24:24 +03:00
446 lines
26 KiB
HTML
446 lines
26 KiB
HTML
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
|
|
<html>
|
|
<head>
|
|
<title>Introduction to Predicate Calculus</title>
|
|
<link href="../docs-assets/Breadcrumbs.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<meta name="viewport" content="width=device-width initial-scale=1">
|
|
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
|
|
<meta http-equiv="Content-Language" content="en-gb">
|
|
|
|
<link href="../docs-assets/Contents.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Progress.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Navigation.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Fonts.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Base.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<script>
|
|
MathJax = {
|
|
tex: {
|
|
inlineMath: '$', '$'], ['\\(', '\\)'
|
|
},
|
|
svg: {
|
|
fontCache: 'global'
|
|
}
|
|
};
|
|
</script>
|
|
<script type="text/javascript" id="MathJax-script" async
|
|
src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
|
|
</script>
|
|
|
|
<link href="../docs-assets/Colours.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
|
|
</head>
|
|
<body class="commentary-font">
|
|
<nav role="navigation">
|
|
<h1><a href="../index.html">
|
|
<img src="../docs-assets/Inform.png" height=72">
|
|
</a></h1>
|
|
<ul><li><a href="../compiler.html">compiler tools</a></li>
|
|
<li><a href="../other.html">other tools</a></li>
|
|
<li><a href="../extensions.html">extensions and kits</a></li>
|
|
<li><a href="../units.html">unit test tools</a></li>
|
|
</ul><h2>Compiler Webs</h2><ul>
|
|
<li><a href="../inbuild/index.html">inbuild</a></li>
|
|
<li><a href="../inform7/index.html">inform7</a></li>
|
|
<li><a href="../inter/index.html">inter</a></li>
|
|
</ul><h2>Inbuild Modules</h2><ul>
|
|
<li><a href="../supervisor-module/index.html">supervisor</a></li>
|
|
</ul><h2>Inform7 Modules</h2><ul>
|
|
<li><a href="index.html"><span class="selectedlink">core</span></a></li>
|
|
<li><a href="../kinds-module/index.html">kinds</a></li>
|
|
<li><a href="../if-module/index.html">if</a></li>
|
|
<li><a href="../multimedia-module/index.html">multimedia</a></li>
|
|
<li><a href="../index-module/index.html">index</a></li>
|
|
</ul><h2>Inter Modules</h2><ul>
|
|
<li><a href="../bytecode-module/index.html">bytecode</a></li>
|
|
<li><a href="../building-module/index.html">building</a></li>
|
|
<li><a href="../codegen-module/index.html">codegen</a></li>
|
|
</ul><h2>Services</h2><ul>
|
|
<li><a href="../arch-module/index.html">arch</a></li>
|
|
<li><a href="../syntax-module/index.html">syntax</a></li>
|
|
<li><a href="../words-module/index.html">words</a></li>
|
|
<li><a href="../html-module/index.html">html</a></li>
|
|
<li><a href="../inflections-module/index.html">inflections</a></li>
|
|
<li><a href="../linguistics-module/index.html">linguistics</a></li>
|
|
<li><a href="../problems-module/index.html">problems</a></li>
|
|
<li><a href="../../../inweb/docs/foundation-module/index.html">foundation</a></li>
|
|
|
|
</ul>
|
|
</nav>
|
|
<main role="main">
|
|
<!--Weave of 'Introduction to Predicate Calculus' generated by Inweb-->
|
|
<div class="breadcrumbs">
|
|
<ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../compiler.html">Inform7 Modules</a></li><li><a href="index.html">core</a></li><li><a href="index.html#11">Chapter 11: Predicate Calculus</a></li><li><b>Introduction to Predicate Calculus</b></li></ul></div>
|
|
<p class="purpose">An exposition of the form of predicate calculus used by Inform.</p>
|
|
|
|
<ul class="toc"><li><a href="11-itpc.html#SP2">§2. Why predicate calculus</a></li><li><a href="11-itpc.html#SP4">§4. Formal description</a></li><li><a href="11-itpc.html#SP7">§7. Free and bound variables, well-formedness</a></li><li><a href="11-itpc.html#SP8">§8. The scope of quantifiers</a></li><li><a href="11-itpc.html#SP10">§10. What is not in our calculus</a></li></ul><hr class="tocbar">
|
|
|
|
<p class="commentary firstcommentary"><a id="SP1"></a><b>§1. </b>"Again and again Haddon thought he had found the key to the strange writings,
|
|
but always he was disappointed. And then one day — he was an old man of seventy
|
|
now — he fed a trial programme into his computer, and for the first time a
|
|
translated sentence was delivered — his life-long task was rewarded. Yes,
|
|
but for the fact that one man had been prepared to devote every spare hour of
|
|
his life to solving the riddle, the amazing story of the Trigan Empire would
|
|
never have been given to the world. WHAT FOLLOWS IS THAT STORY."
|
|
("The Rise and Fall of the Trigan Empire", 1965)
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP2"></a><b>§2. Why predicate calculus. </b>Most attempts to codify the meaning of sentences in any systematic way
|
|
involve predicate calculus, and most people generally seem to agree
|
|
that linguistic concepts (like verbs, adjectives, and determiners)
|
|
correspond uncannily well with logical ones (like binary predicates,
|
|
unary predicates, and quantifiers). Since today's mathematical logic
|
|
has its roots in work on the philosophy of language (chiefly by Frege and
|
|
Wittgenstein), this is not altogether a coincidence. All the same, it is
|
|
striking how good the fit is, considering that human language is so
|
|
haphazard and logic so regular.
|
|
</p>
|
|
|
|
<p class="commentary">At any rate Inform goes along with this consensus, and converts the
|
|
difficult passages in its source text into mathematical propositions
|
|
— lines written in logical notation. This is useful partly as a
|
|
well-defined way to store complicated meanings inside the program, but
|
|
also because these propositions can then be simplified by logical
|
|
rules. We can change their form so long as we do not change their
|
|
meaning, in the hope of finding ways to carry out the same tasks but
|
|
more efficiently than a simple-minded reading of the text would
|
|
suggest.
|
|
</p>
|
|
|
|
<p class="commentary">There are four main tasks to perform:
|
|
</p>
|
|
|
|
<ul class="items"><li>(a) Building propositions from the other Inform data structures;
|
|
</li><li>(b) Simplifying, rearranging and type-checking propositions;
|
|
</li><li>(c) Asserting that certain propositions are true at the start of play;
|
|
</li><li>(d) Compiling certain propositions to I6 code which can test them, make them
|
|
true, or make them false.
|
|
</li></ul>
|
|
<p class="commentary">In this chapter, we take these tasks in order. Because it contains all
|
|
of Inform's predicate calculus lore in one place, it necessarily contains
|
|
little pieces of algorithms from other chapters: a piece of the
|
|
type-checker, a piece of the code for asserting the initial state of
|
|
play, and so on. Well: but the overlap had to go somewhere.
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP3"></a><b>§3. </b>A glimpse of Inform's inner workings can be made by writing a test
|
|
instruction like so:
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>Laboratory is a room. The box is a container.</p>
|
|
</blockquote>
|
|
|
|
<blockquote>
|
|
<p>Test sentence (internal) with a man can see the box in the Laboratory.</p>
|
|
</blockquote>
|
|
|
|
<p class="commentary">At the start of play, the compiled story file will print a textual form of
|
|
the proposition in predicate calculus which that became:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax"> 1. a man can see the box in the Laboratory</span>
|
|
<span class="plain-syntax"> [ Exists x : man(x) & thing('box') & is('laboratory', ContainerOf('box')) & can-see(x, 'box') ]</span>
|
|
<span class="plain-syntax"> x - object.</span>
|
|
</pre>
|
|
<p class="commentary">(The <span class="extract"><span class="extract-syntax">intest</span></span> test case <span class="extract"><span class="extract-syntax">Calculus</span></span> runs about 200 sentences like this.)
|
|
One can similarly "Test description (internal) with..." for any description,
|
|
such as "animals which are in lighted rooms".
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP4"></a><b>§4. Formal description. </b>There are many flavours of predicate calculus, and though they behave in
|
|
broadly similar ways, the details vary in practice. Inform's calculus
|
|
is unusual in several respects, so here is its definition.
|
|
</p>
|
|
|
|
<p class="commentary">The terms "constant", "variable" and "function" below are used in
|
|
their predicate-calculus senses, not their Inform ones. In the excerpt
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>a container in the location of Nicole contains the second noun</p>
|
|
</blockquote>
|
|
|
|
<p class="commentary">the text "location of Nicole" is a phrase deciding an object — a function —
|
|
and "the second noun" is an object that varies — a variable. But if we are
|
|
looking at the sentence only for its logical meaning, we have to forget about
|
|
the passage of time and think about what the sentence means at any single
|
|
moment. "Location of Nicole" and "the second noun" are both fixed, in
|
|
this instant; the only thing which varies is the identity of the possible
|
|
container, because we might have to look at hundreds of different containers
|
|
to see if the sentence is true. One logical translation might be
|
|
$$ \exists x: {\it container}(x)\land {\it in}(x, C_1) \land {\it in}(C_2, x) $$
|
|
where \(C_1\) and \(C_2\) are constants ("location of Nicole" and "second noun"
|
|
respectively), while the only variable is \(x\), the mysterious container.
|
|
(The symbol \(\exists\) means "there exists".) Because objects move
|
|
around in play, and \(C_1\) and \(C_2\) have different values at different
|
|
moments, this sentence is sometimes true and sometimes false. But its
|
|
meaning does not change.
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP5"></a><b>§5. </b>The propositions in our predicate calculus are those which can be made
|
|
using the following ingredients and recipes.
|
|
</p>
|
|
|
|
<p class="commentary">1. There are 26 variables, which we print to the debugging log as <span class="extract"><span class="extract-syntax">x</span></span>, <span class="extract"><span class="extract-syntax">y</span></span>,
|
|
<span class="extract"><span class="extract-syntax">z</span></span>, <span class="extract"><span class="extract-syntax">a</span></span>, <span class="extract"><span class="extract-syntax">b</span></span>, <span class="extract"><span class="extract-syntax">c</span></span>, ..., <span class="extract"><span class="extract-syntax">w</span></span>.
|
|
</p>
|
|
|
|
<p class="commentary">2. The constants are specifications with family <span class="extract"><span class="extract-syntax">VALUE</span></span> — that
|
|
is, all literal constants, variables, list and table entries, or phrases
|
|
which decide values.
|
|
</p>
|
|
|
|
<p class="commentary">3. A "predicate" \(P\) is a statement \(P(a, b, c, ...)\) which is
|
|
either true or false for any given combination \(a, b, c, ...\). The
|
|
"arity" of a predicate is the number of terms it looks at. There is
|
|
speculative talk of allowing higher-order predicates in future (and Inform's
|
|
data structures have been built with one eye on this), but for now
|
|
we use only unary predicates \(U(x)\) or binary predicates \(B(x, y)\), of
|
|
arity 1 and 2 respectively. The predicates in our calculus are as follows:
|
|
</p>
|
|
|
|
<ul class="items"><li>(a) The special binary predicate \({\it is}(x, y)\), true if and only if \(x=y\).
|
|
</li><li>(b) Every kind K (of value or of object) corresponds to a unary
|
|
predicate \(K(x)\).
|
|
</li><li>(c) Every state of an either/or property corresponds to a unary
|
|
predicate, e.g., \({\it open}(x)\).
|
|
</li><li>(d) Every possible value of an enumerated kind of value which
|
|
corresponds to a property similarly corresponds to a unary predicate:
|
|
e.g., if we have defined "colour" as a kind of value and made it a
|
|
property of things, then \({\it green}(x)\), \({\it red}(x)\), and
|
|
\({\it blue}(x)\) might all be unary predicates.
|
|
</li><li>(e) Every adjectival phrase, to which a definition has been
|
|
supplied in the source, likewise produces a unary predicate: for
|
|
example, \({\it visible}(x)\).
|
|
</li><li>(f) An adjective given a definition which involves a threshold for
|
|
a numeric property also produces a binary predicate for its comparative
|
|
form: for instance, a definition for "tall" gives not only a unary
|
|
predicate \({\it tall}(x)\) (as in (e) above) but also a binary predicate
|
|
\({\it taller}(x, y)\).
|
|
</li><li>(g) A special unary predicate \({\it everywhere}(x)\) which asserts that
|
|
the backdrop \(x\) can be found in every room.
|
|
</li><li>(h) Each table column name C gives rise to a binary predicate
|
|
{\it listed-in-C}\((x, y)\), which tests whether value \(x\) is listed in
|
|
the C column of table \(y\). (This looks as if it should really be a
|
|
single ternary predicate, but since we never need to quantify over
|
|
choice of column, nothing would be gained by that.)
|
|
</li><li>(i) Every value property P gives rise to a binary predicate
|
|
{\it same-P-value}\((x, y)\), testing whether objects \(x\) and \(y\)
|
|
have the same value of P. (Again, it would not be useful to quantify
|
|
over P.)
|
|
</li><li>(j) Every direction D gives rise to a binary predicated
|
|
{\it mapped-D}\((x, y)\), testing whether there is a map connection
|
|
from \(x\) to \(y\) in direction D.
|
|
</li><li>(k) Each new relation defined in the source text is a binary
|
|
predicate.
|
|
</li><li>(l) The basic stock of spatial containment relations built into
|
|
Inform — \({\it in}(x, y)\), \({\it on}(x, y)\), etc. — are similarly
|
|
binary predicates.
|
|
</li><li>(m) If \(P\) is a binary predicate present in Inform then so automatically
|
|
is its "reversal" \(R\), defined by \(R(x, y)\) if and only if \(P(y, x)\).
|
|
For instance, the existence of \({\it carries}(x, y)\) ensures that we
|
|
also have {\it carried-by}\((x, y)\), its reversal. The equality predicate
|
|
\(x=y\) is its own reversal, but all other binary predicates are formally
|
|
different from their reversals, even if they always mean the same in
|
|
practice. (The reversal of {\it same-carrying-capacity-as}\((x, y)\) is
|
|
true if and only if the original is true, but we regard them as different
|
|
predicates just the same.)
|
|
</li></ul>
|
|
<p class="commentary">4. If a binary predicate \(B\) has the property that for any \(x\) there
|
|
is at most one \(y\) such that \(B(x, y)\) (for instance, {\it carried-by}
|
|
has this property) then we write \(f_B\) for the function which maps \(x\)
|
|
to either the unique value \(y\) such that \(B(x, y)\), or else to a zero
|
|
value. (In the case where \(y\) is an object, we interpret this as "nothing",
|
|
which for logical purposes is treated as if it were a valid object, so
|
|
that \(f_B\) maps the set of objects to itself.) Another way of saying
|
|
this is that \(f_B\), if it exists, is defined by:
|
|
$$ B(x, y) \Leftrightarrow y = f_B(x). $$
|
|
</p>
|
|
|
|
<p class="commentary">These are the only functions allowed in our predicate calculus, and they
|
|
are always functions of just one variable.
|
|
</p>
|
|
|
|
<p class="commentary">5. A "quantifier" \(Qx\) is a logical expression for the range of values
|
|
of a given variable \(x\): for instance, \(\forall x\) (read "for all \(x\)")
|
|
implies that \(x\) can have any value, whereas \(\exists x\) (read "there
|
|
exists an \(x\)") means only that at least one value works for \(x\). In
|
|
our calculus, we allow not only these quantifiers but also the following
|
|
generalised quantifiers, where \(n\) is a non-negative integer:
|
|
</p>
|
|
|
|
<ul class="items"><li>(a) The quantifier \(V_{=n} x\) —
|
|
meaning "for exactly \(n\) values of \(x\)".
|
|
</li><li>(b) The quantifier \(V_{\geq n} x\) —
|
|
meaning "for at least \(n\) values of \(x\)".
|
|
</li><li>(c) The quantifier \(V_{\leq n} x\) —
|
|
meaning "for at most \(n\) values of \(x\)".
|
|
</li><li>(d) The quantifier \(P_{\geq n} x\) —
|
|
meaning "for at least a percentage of \(n\) values of \(x\)".
|
|
</li><li>(e) The quantifier \(P_{\leq n} x\) —
|
|
meaning "for at most a percentage of \(n\) values of \(x\)".
|
|
</li></ul>
|
|
<p class="commentary">Note that "for all x" corresponds to \(P_{\geq 100} x\), and "there exists
|
|
x" to \(V_{\geq 1} x\), so the above scheme does indeed generalise the
|
|
standard pair of quantifiers \(\forall\) and \(\exists\).
|
|
</p>
|
|
|
|
<p class="commentary">6. A "term" must be a constant, a variable or a function \(f_B(t)\) of
|
|
another term \(t\). So \(x\), "Miss Marple", \(f_B(x)\) and \(f_A(f_B(f_C(6)))\)
|
|
are all examples of terms. We are only allowed to apply functions a finite
|
|
number of times, so any term has the form:
|
|
$$ f_{B_1}(f_{B_2}(... f_{B_n}(s)...)) $$
|
|
for at most a finite number \(n\) of function usages (possibly \(n=0\)), where
|
|
at bottom \(s\) must be either a constant or a variable.
|
|
</p>
|
|
|
|
<p class="commentary">7. A proposition is defined by the following rules:
|
|
</p>
|
|
|
|
<ul class="items"><li>(a) The empty expression is a proposition. This is always true, so in these
|
|
notes it will be written \(\top\).
|
|
</li><li>(b) For any unary predicate \(U\) and any term \(t\), \(U(t)\) is a proposition.
|
|
</li><li>(c) For any binary predicate \(B\) and any terms \(s\), \(t\), \(B(s, t)\)
|
|
is a proposition.
|
|
</li><li>(d) For any proposition \(\phi\), the negation \(\lnot(\phi)\) is a
|
|
proposition. This is by definition true if and only if \(\phi\) is false.
|
|
</li><li>(e) For any propositions \(\phi\) and \(\psi\), the conjunction
|
|
\(\phi\land\psi\) — true if and only if both are true — is a proposition
|
|
so long as it is well-formed (see below).
|
|
</li><li>(f) For any variable \(v\), the quantifier \(\exists v\) is a proposition.
|
|
</li><li>(g) For any variable \(v\), any quantifier \(Q\) other than \(\exists\), and any
|
|
proposition \(\phi\) in which \(v\) is a "free" variable (see below),
|
|
\(Qv\in\lbrace v\mid \phi(v)\rbrace\) is a proposition. The set denotes all
|
|
possible values of \(v\) matching the condition \(\phi(v)\), and this specifies
|
|
the range of the quantifier.
|
|
</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP6"></a><b>§6. </b>Note that there are two ways in which propositions can appear in brackets
|
|
in a bigger proposition: negation (d), and specifying a quantification
|
|
domain (g). We sometimes call the bracketed part a "subexpression" of the
|
|
whole.
|
|
</p>
|
|
|
|
<p class="commentary">In particular, note that — unusually — we do not bracket quantification
|
|
itself. Most definitions would say that given \(v\) and a proposition
|
|
\(\phi(v)\), we can form \(\exists v: (\phi(v))\) — in other words that
|
|
quantification is a way to modify an already created proposition, but that
|
|
\(\exists v\) is not a proposition in its own right, just as \(\lnot\) is not a
|
|
proposition. Inform disagrees. Here \(\exists v\) is a meaningful sentence:
|
|
it means "an object exists". We can form "there is a door" by rule (e),
|
|
conjoining \(\exists x\) and \({\it door}(x)\) to form \(\exists x: {\it door}(x)\).
|
|
(As a nod to conventional mathematical notation, we write a colon after
|
|
a quantifier instead of a conjunction sign \(\land\). But Inform stores it
|
|
as just another conjunction.)
|
|
</p>
|
|
|
|
<p class="commentary">We do bracket the domain of quantification. Most simple predicate
|
|
calculuses (predicates calculus?) have no need, since their only quantifiers
|
|
are \(\forall\) and \(\exists\), and there is a single universe set from which
|
|
all values are drawn. But in Inform, some quantifiers range over doors,
|
|
some over numbers, and so on. In most cases, a quantifier must specify its
|
|
domain. For example,
|
|
$$ \forall x\in \lbrace x\mid {\it number}(x)\rbrace : {\it even}(x) $$
|
|
("all numbers are even" — false, of course) specifies the domain of
|
|
\(\forall\) as the set of all \(x\) such that \({\it number}(x)\).
|
|
</p>
|
|
|
|
<p class="commentary">\(\exists\) is the one exception to this. The statement
|
|
$$ \exists x\in \lbrace x\mid {\it number}(x)\rbrace : {\it even}(x) $$
|
|
("a number is even" — true this time) could equally be written
|
|
$$ \exists x: {\it number}(x)\land {\it even}(x) $$
|
|
("there is an even number"). We take advantage of this, and Inform never
|
|
specifies a domain for a \(\exists\) quantifier.
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP7"></a><b>§7. Free and bound variables, well-formedness. </b>In any proposition \(\phi\), we say that a variable \(v\) is "bound" if it
|
|
appears as the variable governed by a quantifier: it is "free" if it
|
|
does appear somewhere in \(\phi\) — either directly as a term or indirectly
|
|
through a function application — and is not bound. For instance, in
|
|
$$ \forall x : K(x) \land B(x, f_C(y)) $$
|
|
the variable \(x\) is bound and the variable \(y\) is free. In most accounts
|
|
of predicate calculus we say that a proposition is a "sentence" if all
|
|
of its variables are bound, but Inform often needs to parse English text to
|
|
a proposition with one free variable remaining in it, so we are not too
|
|
picky about this.
|
|
</p>
|
|
|
|
<p class="commentary">A well-formed proposition is one in which a variable \(v\) is quantified
|
|
at most once: and in which, if it is quantified, then it occurs only
|
|
after (to the right of) its quantifier, and only within the subexpression
|
|
containing its quantifier. Thus the following are not well-formed:
|
|
$$ \exists v: {\it open}(v)\land \exists v : {\it closed}(v) $$
|
|
(\(v\) is quantified twice),
|
|
$$ {\it open}(v)\land \exists v : {\it closed}(v) $$
|
|
(\(v\) occurs before its quantifier),
|
|
$$ \lnot ( \exists v : {\it closed}(v) ) \land {\it openable}(v) $$
|
|
(\(v\) occurs outside the subexpression containing the quantifier — in this
|
|
case, outside the negation brackets).
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP8"></a><b>§8. The scope of quantifiers. </b>A quantifier introduces a variable into a proposition which would not
|
|
otherwise be there, and it exists only for a limited range. For instance, in
|
|
the proposition
|
|
$$ {\it open}(x)\land\lnot(\exists y: {\it in}(x, y))\land {\it container}(x) $$
|
|
the variable \(y\) exists only within the negation brackets; it ceases to exist
|
|
as soon as we move back out to the container atom. This range is called
|
|
the "scope" of the quantifier. In general, scopes are always as large as
|
|
possible in Inform: a variable lasts until the end of the subexpression in
|
|
which it is created. If the quantifier is outside of any brackets, then the
|
|
variable lasts until the end of the proposition.
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP9"></a><b>§9. </b>Earlier drafts of Inform played games with moving quantifiers around, in
|
|
order to try to achieve more efficiently compiled propositions. The same
|
|
thing is now done by building propositions in a way which places quantifiers
|
|
as far forwards as possible, so we no longer actively move them once they
|
|
are in place. But it seems still worth preserving the rule which says when
|
|
this can be done:
|
|
</p>
|
|
|
|
<p class="commentary">Lemma. Suppose that \(x\) is a variable; \(\phi\) is a proposition in
|
|
which \(x\) is unused; \(\psi(x)\) is a proposition in which \(x\) is free; and that
|
|
\(Q\) is a generalised quantifier. Then
|
|
$$ \phi\land Qx : \psi(x) \quad\Leftrightarrow\quad Qx : \phi\land\psi(x) $$
|
|
provided that \(Q\) requires at least one case in its range to be satisfied.
|
|
</p>
|
|
|
|
<p class="commentary">Proof. In any given evaluation, either \(\phi\) is true, or it is false.
|
|
Suppose it is true. Since \(T\land \theta \Leftrightarrow \theta\), both sides
|
|
reduce to the same expression, \(Qx : \psi(x)\). On the other hand, suppose \(\phi\)
|
|
is false. Then \(\phi\land Qx : \psi(x)\) is false, since \(F\land\theta = F\)
|
|
for any \(\theta\). But the other side is \(Qx : F\). Since we know that \(Q\) can
|
|
only be satisfied if at least one case of \(x\) works, and here every case of
|
|
\(x\) results in falsity, \(Qx : F\) is also false. So the two expressions have
|
|
the same evaluation in this case, too.
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP10"></a><b>§10. What is not in our calculus. </b>The significant thing missing is disjunction. In general, the
|
|
disjunction \(\phi\lor\psi\) — "at least one of \(\phi\) and \(\psi\)
|
|
holds" — is not a proposition.
|
|
</p>
|
|
|
|
<p class="commentary">Natural language does not seem to share the general even-handedness of
|
|
Boolean logic as between "and" and "or", perhaps because of the
|
|
way that speech is essentially a one-dimensional stream of discourse.
|
|
Talking makes it easier to reel off a linear list of requirements than
|
|
to describe a deep tree structure.
|
|
</p>
|
|
|
|
<p class="commentary">Of course, the operations "not" and "and" are between them sufficient
|
|
to express all other operations, and in particular we could imitate
|
|
disjunction like so:
|
|
$$ \lnot (\lnot(\phi)\land\lnot(\psi)) $$
|
|
("they are not both false" being equivalent to "at least one is true"),
|
|
but Inform does not at present make use of this.
|
|
</p>
|
|
|
|
<nav role="progress"><div class="progresscontainer">
|
|
<ul class="progressbar"><li class="progressprev"><a href="10-cap.html">❮</a></li><li class="progresschapter"><a href="P-wtmd.html">P</a></li><li class="progresschapter"><a href="1-cm.html">1</a></li><li class="progresschapter"><a href="2-up.html">2</a></li><li class="progresschapter"><a href="3-bv.html">3</a></li><li class="progresschapter"><a href="4-its.html">4</a></li><li class="progresschapter"><a href="5-lp.html">5</a></li><li class="progresschapter"><a href="6-up.html">6</a></li><li class="progresschapter"><a href="7-ptu.html">7</a></li><li class="progresschapter"><a href="8-ef.html">8</a></li><li class="progresschapter"><a href="9-ita.html">9</a></li><li class="progresschapter"><a href="10-aots.html">10</a></li><li class="progresscurrentchapter">11</li><li class="progresscurrent">itpc</li><li class="progresssection"><a href="11-tr.html">tr</a></li><li class="progresssection"><a href="11-ap.html">ap</a></li><li class="progresssection"><a href="11-pr.html">pr</a></li><li class="progresssection"><a href="11-bas.html">bas</a></li><li class="progresssection"><a href="11-tc.html">tc</a></li><li class="progresssection"><a href="11-sc.html">sc</a></li><li class="progresssection"><a href="11-sm.html">sm</a></li><li class="progresssection"><a href="11-tcp.html">tcp</a></li><li class="progresschapter"><a href="12-ter.html">12</a></li><li class="progresschapter"><a href="13-kak.html">13</a></li><li class="progresschapter"><a href="14-sp.html">14</a></li><li class="progresschapter"><a href="15-pr.html">15</a></li><li class="progresschapter"><a href="16-is.html">16</a></li><li class="progresschapter"><a href="17-tl.html">17</a></li><li class="progresschapter"><a href="18-lc.html">18</a></li><li class="progresschapter"><a href="19-tc.html">19</a></li><li class="progresschapter"><a href="20-eq.html">20</a></li><li class="progresschapter"><a href="21-rl.html">21</a></li><li class="progresschapter"><a href="22-itp.html">22</a></li><li class="progresschapter"><a href="23-ad.html">23</a></li><li class="progresschapter"><a href="24-lv.html">24</a></li><li class="progresschapter"><a href="25-in.html">25</a></li><li class="progresschapter"><a href="26-fc.html">26</a></li><li class="progresschapter"><a href="27-hr.html">27</a></li><li class="progressnext"><a href="11-tr.html">❯</a></li></ul></div>
|
|
</nav><!--End of weave-->
|
|
|
|
</main>
|
|
</body>
|
|
</html>
|
|
|