•
Hover cursor over text of this color to see a popup reference for the symbol or name. Click elsewhere to make the popup disappear.
•
Expand and collapse sections of the argument using the , , and other buttons.
•
The axioms used to prove a given lemma (including the main Goal) are listed before the lemma or as children of the lemma. The ones listed before are those that define or introduce symbols that are used in the statement of the lemma (i.e. the ones that are required for understanding the lemma).
•
An Assertion is an axiom that I expect to be uncontroversial relative to the axioms designated Assumption. It is a vague and subjective designation. If the language interpretation guide entries (the informal textual semantics) for the symbols that the axiom depends on do not make it clear to you that this axiom should be true, then you should criticize this designation. Depending on the specifics of your criticism, I can respond by improving the entries in the language interpretation guide for some of those symbols, or else by changing the designation to "Assumption" or "Claim".
•
A Definitional Axiom is an axiom that should be be absolutely uncontroversial among the intended audience for this argument. Usually, if not always, it will have a very objective/mathematical character.
•
✓Lemma and ✓Goal denote sentences that have been formally proved (computer checkable) to be logical consequences of the definitions, axioms and lemmas that precede them, and the definitions, axioms and lemmas that are their children (immediate descendants only). A Lemma has an informal proof. A Claim is a statement that is used as a Lemma but has neither been formally nor informally proved.
•
A Defn~ introduces a symbol together with a sentence that intuitively defines it, but does not technically yield a definitional extension of the theory. Usually such symbols could be turned into proper definitions with the use of a definite description operator.
Formalization of deductive argument from
D.N. Walton. Informal Logic: A Pragmatic Approach. Cambridge University
Press, 2008.
which goes like this:
Getting married involves promising to live with a person for the rest of your life.
Nobody can safely predict compatibility with another person for life.
One should not make a promise unless one can safely predict that one will keep it.
If two people aren’t compatible, they can’t live together.
One should not promise to do something one cannot do.
Therefor, nobody should ever get married.
Sort Person
People. The axioms are more-literally true if we take it to be the set of people who are not clearly near death. Otherwise Assumption 1 is easily disputable, for example. We should also specify that they are devout Catholics, or something like that, in order for Assertion 1 to be clearly acceptable.
People. The axioms are more-literally true if we take it to be the set of people who are not clearly near death. Otherwise Assumption 1 is easily disputable, for example. We should also specify that they are devout Catholics, or something like that, in order for Assertion 1 to be clearly acceptable.
Sort Date - Dates, e.g. 1 Sept 1998
Dates, e.g. 1 Sept 1998
Sort Act
(Classes of) potential actions that, like verbs, are not associated with a particular Person, but unlike most verbs
are associated with a particular Date. E.g. "Flying to Ghent on July 6."
(Classes of) potential actions that, like verbs, are not associated with a particular Person, but unlike most verbs
are associated with a particular Date. E.g. "Flying to Ghent on July 6."
Sort Prop
Propositions about the real world; things that will turn out true or false. It is important that they are distinct from 0-ary predicate symbols, as we will have functions that operate on Prop that cannot treat all elements of Prop as just belonging to one of two equivalence classes (depending on whether they are satisfied or not).
Propositions about the real world; things that will turn out true or false. It is important that they are distinct from 0-ary predicate symbols, as we will have functions that operate on Prop that cannot treat all elements of Prop as just belonging to one of two equivalence classes (depending on whether they are satisfied or not).
Variables p, q, p₁, p₂ are reserved for sort Person.
PersonPersonPersonPerson
Variables d, d₁, d₂ are reserved for sort Date.
DateDateDate
Variables a, a₁, a₂ are reserved for sort Act.
ActActAct
Variables ψ, φ are reserved for sort Prop.
PropProp
Doesp(a) : Person × Act → 𝔹 - p performs the action a (on the date specified by a).
Person × Act → 𝔹
p performs the action a (on the date specified by a).
LiveWithp₁,p₂(d₁, d₂) : Person × Person × Date × Date → 𝔹
Iff p₁ and p₂ are both alive and share the same main residence during the period from d₁ to d₂, inclusive. False if d₁ > d₂.
Person × Person × Date × Date → 𝔹
Iff p₁ and p₂ are both alive and share the same main residence during the period from d₁ to d₂, inclusive. False if d₁ > d₂.
Holds(ψ) : Prop → 𝔹 - The given proposition is true (will turn out true).
Prop → 𝔹
The given proposition is true (will turn out true).
Compatiblep₁,p₂(d₁, d₂) : Person × Person × Date × Date → 𝔹 - p₁ and p₂ are compatible during the period from d₁ to d₂.
Person × Person × Date × Date → 𝔹
p₁ and p₂ are compatible during the period from d₁ to d₂.
CanSafelyPredictp(ψ, d) : Person × Date × Prop → 𝔹 - On date d, p can safely predict that ψ will be satisfied.
Person × Date × Prop → 𝔹
On date d, p can safely predict that ψ will be satisfied.
ShouldNotDop(a) : Person × Act → 𝔹 - iff you think p should not do action a
Person × Act → 𝔹
iff you think p should not do action a
getMarriedTop(d) : Person × Date → Act - The action of getting married to p on date d.
Person × Date → Act
The action of getting married to p on date d.
makePromised(ψ) : Date × Prop → Act
To make an utterance, on date d, like “I promise that ψ”, which is directed at someone with the intention of their interpreting it as a sincere and literal statement.
Date × Prop → Act
To make an utterance, on date d, like “I promise that ψ”, which is directed at someone with the intention of their interpreting it as a sincere and literal statement.
min(d₁,d₂) : Date × Date → Date - The earlier of the two dates.
Date × Date → Date
The earlier of the two dates.
dateOfDeath(p) : Person → Date - Date when the person dies.
Person → Date
Date when the person dies.
Defn firstDeath(p, q) : Person × Person → Date - Date when the first of the two people die.
If Personp₁ marries p₂ (on date d), then p₁ makes the promise (on date d) that they will live together until one of them dies.
Assumption 1: Roughly: You can't safely predict that two people will be compatible till death. More precisely: No person p₁, on any date, can safely predict that he or she will be compatible with another person p₂ until one of their deaths.
Roughly: You can't safely predict that two people will be compatible till death. More precisely: No person p₁, on any date, can safely predict that he or she will be compatible with another person p₂ until one of their deaths.
Assumption 2: If p cannot (on date d) safely predict that ψ will be true, then p should not (on date d) promise that ψ will be true.