•
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.

• 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

• A

•

• A

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.

Sort Date - 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."

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).

Variables p, q, p₁, p₂ are reserved for sort Person.

Variables d, d₁, d₂ are reserved for sort Date.

Variables a, a₁, a₂ are reserved for sort Act.

Variables ψ, φ are reserved for sort Prop.

Does_{p}(a) : Person × Act → 𝔹 - p performs the action a (on the date specified by a).

LiveWith_{p₁,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₂.

Holds(ψ) : Prop → 𝔹 - The given proposition is true (will turn out true).

Compatible_{p₁,p₂}(d₁, d₂) : Person × Person × Date × Date → 𝔹 - p₁ and p₂ are compatible during the period from d₁ to d₂.

CanSafelyPredict_{p}(ψ, d) : Person × Date × Prop → 𝔹 - On date d, p can safely predict that ψ will be satisfied.

ShouldNotDo_{p}(a) : Person × Act → 𝔹 - iff you think p should not do action a

getMarriedTo_{p}(d) : Person × Date → Act - The action of getting married to p on date d.

makePromise^{d}(ψ) : 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.

dateOfDeath(p) : Person → Date - Date when the person dies.

Defn firstDeath(p, q) : Person × Person → Date - Date when the first of the two people die.

∀p,q. firstDeath(p, q) = min(dateOfDeath(p),dateOfDeath(q))

Defn~ liveWithTillDeath_{p₁,p₂}(d) : Person × Person × Date → Prop - p₁ and p₂ LiveWith each other from d until the first of them dies.

∀p₁,p₂,d. Holds(liveWithTillDeath_{p₁,p₂}(d)) ⇔ LiveWith_{p₁,p₂}(d, firstDeath(p₁, p₂))

Defn~ compatibleTillDeath_{p₁,p₂}(d) : Person × Person × Date → Prop - p₁ and p₂ are Compatible with each other from d until the first of them dies.

∀p₁,p₂,d. Holds(compatibleTillDeath_{p₁,p₂}(d)) ⇔ Compatible_{p₁,p₂}(d, firstDeath(p₁, p₂))

✓Goal: Nobody should ever get married!

∀p,q,d. ShouldNotDo_{p}(getMarriedTo_{q}(d))

Assertion 1: If Person p₁ marries p₂ (on date d), then p₁ makes the promise (on date d) that they will live together until one of them dies.

∀p₁,p₂,d. Does_{p₁}(getMarriedTo_{p₂}(d)) ⇒ Does_{p₁}(makePromise^{d}(liveWithTillDeath_{p₁,p₂}(d)))

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.

∀p₁,p₂,d. ¬CanSafelyPredict_{p₁}(compatibleTillDeath_{p₁,p₂}(d), d)

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.

∀p,d,ψ. ¬CanSafelyPredict_{p}(ψ, d) ⇒ ShouldNotDo_{p}(makePromise^{d}(ψ))

Assumption 3: Two people who are incompatible during a period cannot live together during that period.

∀p₁,p₂,d₁,d₂. ¬Compatible_{p₁,p₂}(d₁, d₂) ⇒ ¬LiveWith_{p₁,p₂}(d₁, d₂)

Assertion 2: If p (on date d) can safely predict that ψ will hold, and ψ impies φ, then p (on date d) can safely predict that φ will hold.

∀p,d,ψ,φ. CanSafelyPredict_{p}(ψ, d) ∧ (Holds(ψ) ⇒ Holds(φ)) ⇒ CanSafelyPredict_{p}(φ, d)

Assertion 3: If p should not do action a₂, and doing a₁ requires doing a₂, then p should not do a₁.

∀p,a₁,a₂. ShouldNotDo_{p}(a₂) ∧ (Does_{p}(a₁) ⇒ Does_{p}(a₂)) ⇒ ShouldNotDo_{p}(a₁)