Basic Mathematical Logic - Understanding Sequents

[Math Amateur]

I am reading the book Mathematical Logic by Ian Chiswell and Wilfred Hodges ... and am currently focused on Chapter 2: Informal Natural Deduction ...

I need help with interpreting the notation of an aspect of Exercise 2.1.3 which reads as follows:View attachment 4996In the above text after the text: "Possible sequent rule B:" we read the following:

"If the sequent $$( \{ \phi \} \vdash \psi )$$ ... ... "How do I interpret $$( \{ \phi \} \vdash \psi )$$ ... Chiswell and Hodges point out that $$( \phi \vdash \psi )$$ means "there is a proof whose conclusion is $$\psi$$ and whose undischarged assumptions are all in the set $$\phi$$" ... or ... "$$ \phi$$ entails $$\psi$$" ... ...

... BUT ... what is meant by a sequent like $$( \{ \phi \} \vdash \psi )$$ where the assumptions are a set \{ \phi \} ... that is a set of a set of assumptions ... ...

Can someone clarify this notation ... what does it mean exactly ..

Peter

 

[Deveno]

Here is a set of assumptions:

(the axioms of group theory)

Typically, this is formulated as (or can be formalized as) 3 or 4 well-formed formulae.

Here is a set of sets of assumptions:

{(the axioms of group theory),(the axioms of the natural numbers)}

For example, from the second set we can prove "the laws of exponents":

For all $g \in G$, where $G$ is a group, and all natural numbers $k,m$:

$g^kg^m = g^{k+m}$

$(g^k)^m = g^{km}$.

We cannot prove these from the first set alone, in fact, strictly speaking, they aren't even expressible solely in terms of the axioms of a group.

In logic, individual expressions can be quite convoluted: the very statement of the completeness of the real numbers, for example, is beyond the ability of first-order logic to even capture, and other simple facts like "we can always pick a smallest natural number from a finite set of natural numbers" take up a lot of space written in formal terms. So we tend to "package" individual statements as something like $p$ for convenience, and we tend to package collections of statements that commonly occur together as something like $\phi$. Similarly, a "theory" is a collection of a collection of related statements (group theory is somewhat of an exception, the basic axioms can be simply expressed as a single set-vector spaces, on the other hand, require a set of sets of assumptions:

{(abelian group theory), (field theory), (vector space axioms)}).

A lot of work over the centuries has gone into:

a) "condensing" high-level (many-tiered) theories into compact expression

b) "reducing" high-level theories (that we often talk about in "natural language") to their explicit low-level formal expression (often, for the purpose of automatic proof-verification).

A "set of sets" is still a set, so at least for this particular example, you could just replace $\{\phi\}$ by something like $\Gamma$, what I *believe* they are are getting at, in this example however, is $\{phi\}$ is the set of assumptions whose sole member is the single assumption $\phi$.

One caveat: some people use set theory to define logic, others the other way around. This is a *big* can o' worms, if one is using set theory to frame logic it's often convenient to have these things called *ur-elements*, so one can have sets with "things" in them (typically "letters" from an "alphabet", but, for example, ur-elements might be "elephants" or "Frank"). Typically, one can then form "atomic statements" in logic, using such ur-elements, such as:

"Frank = Frank".

I want to point out it's only *convenient* to do this, it's not, strictly, speaking, necessary. The various logical connectives (conjunction, disjunction, implication, equivalence) are then cast as various set-operations. This is, essentially, the path taken in computer programming, where these logical operations are modeled by physical circuitry, called "gates" (perhaps someone can confirm this? It's been awhile...).

Using logic to define set theory is the path most mathematicians embark on. The grounding of said logic is then, essentially, our innate ability to reason and communicate, that is-we rely on natural linguistics to define by analogy. In a sense, then, it might properly be said we have *no idea* what logic and sets actually *are* (in an ontological sense), but rather, have an intuition as to what they *ought to be*.

 

[Math Amateur]

Here is a set of assumptions:

(the axioms of group theory)

Typically, this is formulated as (or can be formalized as) 3 or 4 well-formed formulae.

Here is a set of sets of assumptions:

{(the axioms of group theory),(the axioms of the natural numbers)}

For example, from the second set we can prove "the laws of exponents":

For all $g \in G$, where $G$ is a group, and all natural numbers $k,m$:

$g^kg^m = g^{k+m}$

$(g^k)^m = g^{km}$.

We cannot prove these from the first set alone, in fact, strictly speaking, they aren't even expressible solely in terms of the axioms of a group.

In logic, individual expressions can be quite convoluted: the very statement of the completeness of the real numbers, for example, is beyond the ability of first-order logic to even capture, and other simple facts like "we can always pick a smallest natural number from a finite set of natural numbers" take up a lot of space written in formal terms. So we tend to "package" individual statements as something like $p$ for convenience, and we tend to package collections of statements that commonly occur together as something like $\phi$. Similarly, a "theory" is a collection of a collection of related statements (group theory is somewhat of an exception, the basic axioms can be simply expressed as a single set-vector spaces, on the other hand, require a set of sets of assumptions:

{(abelian group theory), (field theory), (vector space axioms)}).

A lot of work over the centuries has gone into:

a) "condensing" high-level (many-tiered) theories into compact expression

b) "reducing" high-level theories (that we often talk about in "natural language") to their explicit low-level formal expression (often, for the purpose of automatic proof-verification).

A "set of sets" is still a set, so at least for this particular example, you could just replace $\{\phi\}$ by something like $\Gamma$, what I *believe* they are are getting at, in this example however, is $\{phi\}$ is the set of assumptions whose sole member is the single assumption $\phi$.

One caveat: some people use set theory to define logic, others the other way around. This is a *big* can o' worms, if one is using set theory to frame logic it's often convenient to have these things called *ur-elements*, so one can have sets with "things" in them (typically "letters" from an "alphabet", but, for example, ur-elements might be "elephants" or "Frank"). Typically, one can then form "atomic statements" in logic, using such ur-elements, such as:

"Frank = Frank".

I want to point out it's only *convenient* to do this, it's not, strictly, speaking, necessary. The various logical connectives (conjunction, disjunction, implication, equivalence) are then cast as various set-operations. This is, essentially, the path taken in computer programming, where these logical operations are modeled by physical circuitry, called "gates" (perhaps someone can confirm this? It's been awhile...).

Using logic to define set theory is the path most mathematicians embark on. The grounding of said logic is then, essentially, our innate ability to reason and communicate, that is-we rely on natural linguistics to define by analogy. In a sense, then, it might properly be said we have *no idea* what logic and sets actually *are* (in an ontological sense), but rather, have an intuition as to what they *ought to be*.

Thanks Deveno,

Appreciate your substantial help ...

Still reflecting on what you have said ...

Peter

 

[Evgeny.Makarov]

Chiswell and Hodges point out that $$( \phi \vdash \psi )$$ means "there is a proof whose conclusion is $$\psi$$ and whose undischarged assumptions are all in the set $$\phi$$

I doubt they say this because in the picture you showed $\phi$ and $\psi$ range over individual formulas while $\Gamma$ and $\Delta$ range over sets of formulas. A sequent is an ordered pair of a set (or, in some presentations, a multiset or an ordered sequence) of formulas and a formula. That's why formally one is supposed to wrap formulas left of the turnstile in curly braces. In many textbooks, though, these braces are dropped and union of sets is simply denoted by a comma.

 

[Deveno]

I doubt they say this because in the picture you showed $\phi$ and $\psi$ range over individual formulas while $\Gamma$ and $\Delta$ range over sets of formulas. A sequent is an ordered pair of a set (or, in some presentations, a multiset or an ordered sequence) of formulas and a formula. That's why formally one is supposed to wrap formulas left of the turnstile in curly braces. In many textbooks, though, these braces are dropped and union of sets is simply denoted by a comma.

I suspect this may be similar to the convention of writing a function $f: \Bbb R^2 \to \Bbb R^2$ as $f(x,y)$ rather than $f((x,y))$, or the group generated by elements $a$ and $b$ as $\langle a,b\rangle$ rather than $\langle\{a,b\}\rangle$. Hard to say without seeing the original text, though.

 

[Math Amateur]

I doubt they say this because in the picture you showed $\phi$ and $\psi$ range over individual formulas while $\Gamma$ and $\Delta$ range over sets of formulas. A sequent is an ordered pair of a set (or, in some presentations, a multiset or an ordered sequence) of formulas and a formula. That's why formally one is supposed to wrap formulas left of the turnstile in curly braces. In many textbooks, though, these braces are dropped and union of sets is simply denoted by a comma.

Hi Evgeny,

Thanks fpr the help ...

Reflecting on what you have said I checked my text (Mathematical Logic by Ian Chiswell and Wilfred Hodges) and it seems that C&H are using Greek capital letters like $$\Gamma$$ and $$\Delta$$ for sets of statements or formulas and small Greek letters like $$\phi$$ and $$\psi$$ for single statements or formulas ... checking through the pages of C&H it looks as if this is the case as braces only appear around lower case Greek letters ... although C&H never mention nor explain this notational convention

Indeed the definition of a sequent uses $$\Gamma$$ and no braces as follows:View attachment 5005I should have picked this notational convention up since most texts I have read that have sections or chapters on set theory use capital letters (usually English capitals) for sets and lower case letters (again, usually English) for elements ..

I guess it would have been easier if the text had mentioned/explained the convention ...

Thanks again for your help ...

Peter