rzach / forallx-yyc

UCalgary version of forallx, an introduction to formal logic
https://forallx.openlogicproject.org/
Creative Commons Attribution 4.0 International
94 stars 30 forks source link

Semantics for Quantifiers #12

Closed wyleyr closed 5 years ago

wyleyr commented 7 years ago

Via email, I said:

I like that the book uses a substitutional approach rather than dealing with assignment functions. But I am finding that, as things are set up in the text, this doesn't actually buy much in terms of simplifying semantic reasoning about quantifiers, because we don't assume that every object has a name. (Compare the approach in Forbes' "Modern Logic", which just uses straight substitutional clauses for the quantifiers, because he adopts an 'alphabetic convention' that ensures every object has a name.) The net result is that when you apply the book's clauses for the quantifiers, you end up quantifying over additional interpretations in the metalanguage, rather than objects in the original interpretation, and this makes the reasoning a bit clumsy and, I think, more opaque to students.

The approach I think I've settled on for teaching this to the students next week is to keep the basic substitutional approach, but introduce a notation that makes what it means to 'extend' an interpretation a bit more obvious, and use this in the semantic clauses for the quantifiers, like

'\exists x F(...x...)' is true is an interpretation M iff: for some object \delta in the domain of M, 'F(...d...)' is true in M[d: \delta]

'\forall x F(...x...)' is true is an interpretation M iff: for every object \delta in the domain of M, 'F(...d...)' is true in M[d: \delta]

This avoids talking about assignment functions but still quantifies over the objects in the domain of M in the metalanguage, rather than over alternative interpretations M'.

Richard Zach said:

This also should not be too hard. Changes only required in 28.3, 30 passim, and 31.

An alternative would be to define what it means for an object in the domain to satisfy a formula with a free variable (\delta satisfies A(x) iff M[d:\delta] |= A(d)) in 28.3. From then on you can just talk about satisfaction.

Talking about satisfaction also makes it easier to talk about expressive power, which I'd like to do at some point. That is, I'd like to add a section about the extensions of formulas and not just of predicates, e.g., A(x) has as extension {\alpha : \alpha satisfies A(x)} (etc for more than one variable).

wyleyr commented 7 years ago

Talking about satisfaction would also make it easy to define when a formula or sentence is satisfiable, which is a semantic concept currently missing from Chapter 29 -- and actually, now that I think about it, Chapter 11.

(The introductory chapters of the book talk about contingent sentences, but no analogue of contingency is ever defined for TFL and FOL. The closest we come is "joint consistency", but it's a bit strange to talk about a single sentence being "jointly consistent". You can say it's neither a contradiction nor a logical truth, but that gets pretty long-winded and feels a bit backward.)

rzach commented 7 years ago

I want to add satisfiability of sentences anyway. It's really important if you want to use logic for applications outside of philosophy, eg, when you want to apply SAT solvers. (However, the two notions--satisfiability of sentences, and satisfaction of a formula by an object--are independent.)

rzach commented 5 years ago

Fixed with commit fa99c0b