Well-formed Formulas Set in Formal Theory

  • I
  • Thread starter Calculuser
  • Start date
  • #1
49
3
There is a statement on page 26 in Elliott Mendelson's book of "Introduction to Mathematical Logic" as shown:

Ekran Alıntısı.PNG


What I got from the statement above, which is obvious, I guess, is that in the sequence of [itex]\mathcal{B}_1,\mathcal{B}_2,...\mathcal{B}_k[/itex] there are "SOME" well-formed formulas (wfs) that elements of [itex]\Gamma[/itex] set of wfs, or axioms that are NOT elements of [itex]\Gamma[/itex], or direct consequences by some rule of inference of some the preceding wfs in the sequence. To me, It also seem to be possible that "ALL" of those [itex]\mathcal{B}_k[/itex] wfs can by definition be one of the three possibilities mentioned above. Hence, we cannot say [itex]\Gamma=\{\mathcal{B}_1,\mathcal{B}_2,...\mathcal{B}_k\}[/itex].

My questions in regard to these are:

1) Does [itex]\mathcal{L}(\mathcal{B}_k=\mathcal{L})[/itex] has to be in the set of [itex]\Gamma[/itex] or not?
2) What exactly does [itex]\Gamma[/itex] represent?
 
  • Like
Likes Periwinkle

Answers and Replies

  • #2
13,574
10,691
There is a statement on page 26 in Elliott Mendelson's book of "Introduction to Mathematical Logic" as shown:

View attachment 242202

What I got from the statement above, which is obvious, I guess, is that in the sequence of [itex]\mathcal{B}_1,\mathcal{B}_2,...\mathcal{B}_k[/itex] there are "SOME" well-formed formulas (wfs) that elements of [itex]\Gamma[/itex] set of wfs, or axioms that are NOT elements of [itex]\Gamma[/itex], or direct consequences by some rule of inference of some the preceding wfs in the sequence. To me, It also seem to be possible that "ALL" of those [itex]\mathcal{B}_k[/itex] wfs can by definition be one of the three possibilities mentioned above. Hence, we cannot say [itex]\Gamma=\{\mathcal{B}_1,\mathcal{B}_2,...\mathcal{B}_k\}[/itex].
... which wasn't said.
My questions in regard to these are:

1) Does [itex]\mathcal{L}(\mathcal{B}_k=\mathcal{L})[/itex] has to be in the set of [itex]\Gamma[/itex] or not?
No. ##\mathscr C \in \{\, \mathscr B_k\,\}##.
2) What exactly does [itex]\Gamma[/itex] represent?
##\Gamma## represents given conditions. E.g. for any linear map ##\varphi## we have ##\varphi(0)=0## means '##\varphi## is linear' ##\in \Gamma##. It also means that impossible statements can be part of ##\Gamma##. E.g. if any pink unicorn is part of equidae, then it has four hooves, means that 'pink unicorns are part of equidae' is an element of ##\Gamma .##
 
  • #3
49
3
... which wasn't said.
Did you mean the entire text or just [itex]\Gamma=\{\mathcal{B}_1,\mathcal{B}_2,...\mathcal{B}_k\}[/itex]? Could you clarify a bit?

[itex]\Gamma[/itex] represents given conditions. E.g. for any linear map [itex]\varphi[/itex] we have [itex]\varphi(0)=0[/itex] means '[itex]\varphi[/itex] is linear' [itex]\in\Gamma[/itex]. It also means that impossible statements can be part of [itex]\Gamma[/itex]. E.g. if any pink unicorn is part of equidae, then it has four hooves, means that 'pink unicorns are part of equidae' is an element of [itex]\Gamma[/itex].
Then [itex]\Gamma[/itex] is like a universal set of any statements that are either true or false.

No. [itex]\mathscr C \in \{\mathscr B_k\}[/itex].
In light of what I understood in the comment on your explanation of [itex]\Gamma[/itex] above, that seemed absurd to me. Why can [itex]\mathscr C[/itex] not be an element of [itex]\Gamma[/itex], as it is a universal set of statements?
 
  • #4
stevendaryl
Staff Emeritus
Science Advisor
Insights Author
8,401
2,581
Then [itex]\Gamma[/itex] is like a universal set of any statements that are either true or false.
What does "universal set" mean?

##\Gamma## is a set of assumptions or axioms, and you're trying to figure out what can be derived from those assumptions.

So, for example, if I tell you:
  1. Sam is a dog.
  2. If Sam is a dog, then Sam is a mammal.
  3. If Sam is a mammal, then Sam is a vertebrate.
  4. If Sam is a vertebrate, then Sam has bones.
Then let ##\Gamma## be the collection of statements 1-4.

A consequence of this is: ##\mathcal{C}: ## "Sam has bones". To prove this, let

##B_1 = ## "Sam is a dog"
##B_2 = ## "If Sam is a dog, then Sam is a mammal"
##B_3 = ## "Sam is a mammal".
##B_4 = ## "If Sam is a mammal, then Sam is a vertebrate."
##B_5 = ## "Sam is a vertebrate."
##B_6 = ## "If Sam is a vertebrate, then Sam has bones."
##B_7 = ## "Sam has bones"

Then the sequence ##B_1 ... B_7## is a proof of ##\mathcal{C}## provided that:
  • ##\mathcal{C} = B_7##
  • Every statement ##B_i## is either in ##\Gamma##, or follows from previous statements.
We can check:
  1. ##B_1## is in ##\Gamma## (check)
  2. ##B_2## is in ##\Gamma## (check)
  3. ##B_3## follows from ##B_1## and ##B_2## (check)
  4. ##B_4## is in ##\Gamma## (check)
  5. ##B_5## follows from ##B_3## and ##B_4## (check)
  6. ##B_6## is in ##\Gamma## (check)
  7. ##B_7## follows from ##B_5## and ##B_6## (check)
  8. ##B_7 = \mathcal{C}## (check)
So we've shown that ##\mathcal{C}## is a consequence of ##\Gamma##.
 
  • #5
49
3
What does "universal set" mean?
What I mean by that is a set of anything related to the real of propositions, e.g. atomic formulas, statement forms, etc. from which we deduce a consequence with some propositions within. Because in the screenshot I posted above it does NOT say that ALL [itex]
\mathcal{B}_1,\mathcal{B}_2,...\mathcal{B}_k[/itex] belong to [itex]\Gamma[/itex], yet uses "for each [itex]i[/itex], [itex]\mathcal{B}_i[/itex] is EITHER an axiom OR [itex]\mathcal{B}_i[/itex] in [itex]\Gamma[/itex], OR [itex]\mathcal{B}_i[/itex] is a direct consequence..." phrase. Then I tend to think that there is a possibility of [itex]\mathcal{B}_i[/itex] as an axiom, but not an element of [itex]\Gamma[/itex]. I do not know whether or not this is possible, if it can, then how.

We can check:
  1. [itex]B_1[/itex] is in [itex]\Gamma[/itex] (check)
  2. [itex]B_2[/itex] is in [itex]\Gamma[/itex] (check)
  3. [itex]B_3[/itex] follows from [itex]B_1[/itex] and [itex]B_2[/itex] (check)
  4. [itex]B_4[/itex] is in [itex]\Gamma[/itex] (check)
  5. [itex]B_5[/itex] follows from [itex]B_3[/itex] and [itex]B_4[/itex] (check)
  6. [itex]B_6[/itex] is in [itex]\Gamma[/itex] (check)
  7. [itex]B_7[/itex] follows from [itex]B_5[/itex] and [itex]B_6[/itex] (check)
  8. [itex]B_7= \mathcal{C}[/itex] (check)
Where do these [itex]B_3,B_5,B_7[/itex] belong, then, if not to [itex]\Gamma[/itex]?
 
  • #6
stevendaryl
Staff Emeritus
Science Advisor
Insights Author
8,401
2,581
Because in the screenshot I posted above it does NOT say that ALL [itex]
\mathcal{B}_1,\mathcal{B}_2,...\mathcal{B}_k[/itex] belong to [itex]\Gamma[/itex], yet uses "for each [itex]i[/itex], [itex]\mathcal{B}_i[/itex] is EITHER an axiom OR [itex]\mathcal{B}_i[/itex] in [itex]\Gamma[/itex], OR [itex]\mathcal{B}_i[/itex] is a direct consequence..." phrase. Then I tend to think that there is a possibility of [itex]\mathcal{B}_i[/itex] as an axiom, but not an element of [itex]\Gamma[/itex].
No, the rules explicitly say that each ##B## must either be an element of ##\Gamma##, or derivable from previous sentences by the rules of inference. For the sake of the definition of "consequence", ##\Gamma## is the only set of axioms you have.

Where do these [itex]B_3,B_5,B_7[/itex] belong, then, if not to [itex]\Gamma[/itex]?
##\Gamma## in my example is the set ##\{ B_1, B_2, B_4, B_6 \}##. So ##B_3, B_5, B_7## are NOT in ##\Gamma##, but they are derivable from other ##B##'s.
 
  • #7
49
3
No, the rules explicitly say that each ##B## must either be an element of ##\Gamma##, or derivable from previous sentences by the rules of inference. For the sake of the definition of "consequence", ##\Gamma## is the only set of axioms you have.



##\Gamma## in my example is the set ##\{ B_1, B_2, B_4, B_6 \}##. So ##B_3, B_5, B_7## are NOT in ##\Gamma##, but they are derivable from other ##B##'s.
I agree on that part! However, I do not get why it was extra(?) stated that [itex]\mathcal{B}_i[/itex] can also be an axiom in the original text of the author as said "...either [itex]\mathcal{B}_i[/itex] is an axiom..." in addition to the things you said. Wouldn't it be sufficient to say that [itex]\mathcal{B}_i[/itex] is either a well-formed formula from [itex]\Gamma[/itex] or a direct consequence by some rule of inference as you stated?
 
  • #8
stevendaryl
Staff Emeritus
Science Advisor
Insights Author
8,401
2,581
I agree on that part! However, I do not get why it was extra(?) stated that [itex]\mathcal{B}_i[/itex] can also be an axiom in the original text of the author as said "...either [itex]\mathcal{B}_i[/itex] is an axiom..." in addition to the things you said. Wouldn't it be sufficient to say that [itex]\mathcal{B}_i[/itex] is either a well-formed formula from [itex]\Gamma[/itex] or a direct consequence by some rule of inference as you stated?
Wow. I'm sorry. I read it over too quickly. It does say that ##B_i## can be an axiom. In that case, I'm not sure about the motivation for introducing ##\Gamma##. Why not let ##\Gamma## include all the axioms?

The author may be distinguish "logical" from "nonlogical" axioms, where a logical axiom defines when something is true for every possible theory.
 
  • #9
63
13

One theory described in the Proposition Calculus can be accurately illustrated by chess

  • The language is the sequence of symbols that can be used to describe a chess game position.
  • Well-formed formulas correspond to real, possible positions. So there is only one white and one black king on the board, not five of white and black.
  • Axioms: A series of chess game positions.
  • Hypothesis: specific chess game positions.
  • Conclusion rules: rules for chess steps.
  • Proof: To derive a particular chess game position from axioms and hypotheses based on rules for chess play. (So how chess pieces can move.)
Perhaps I am not even mistaken that Hilbert was motivated by the analogy with chess when he created the Hilbert program.
 
Last edited:
  • #10
1,656
921
... which wasn't said.

No. ##\mathscr C \in \{\, \mathscr B_k\,\}##.

##\Gamma## represents given conditions. E.g. for any linear map ##\varphi## we have ##\varphi(0)=0## means '##\varphi## is linear' ##\in \Gamma##. It also means that impossible statements can be part of ##\Gamma##. E.g. if any pink unicorn is part of equidae, then it has four hooves, means that 'pink unicorns are part of equidae' is an element of ##\Gamma .##
If a white horse is not a horse, then a pink unicorn is not a unicorn, and an Easter egg is not an egg.

##(\forall x)[(Wx\land Hx) \Rightarrow \neg Hx]\Rightarrow ((\forall x)[(Px\land Ux) \Rightarrow \neg Ux] \land (\forall x)[(\mathcal E x\land Ex) \Rightarrow \neg Ex])##

440px-Adolphe_Millot_oeufs-fixed.jpg
 
  • #11
13,574
10,691
Wow. I'm sorry. I read it over too quickly. It does say that ##B_i## can be an axiom. In that case, I'm not sure about the motivation for introducing ##\Gamma##. Why not let ##\Gamma## include all the axioms?
Loosely speaking, a proof consists of a framework given by axioms, assumptions as basis for conclusions under these assumptions, here ##\Gamma##, and previous or intermediate results ##\mathscr{B}_i## including the last conclusion ##\mathscr{B}_k##.

Neither ##\Gamma## nor the ##\mathscr{B}_i## include axioms, as they are of a different kind. Axioms build the framework, or calculus, or setup of what follows. They have to be minimal in number and without contradictions. This is not true for ##\Gamma\,.## If ##\text{ False } \in \Gamma##, then we still can get a valid proof. Indeed it happens regularly in mathematics, that a conclusion is drawn without bothering existence! This is often part of a second consideration afterwards. E.g. in the theory of simple Lie algebras, all possible root systems are classified before one proves, that each of them actually represents a specific Lie algebra. The ##\mathscr{B}_i## are results which already have been concluded from axioms and ##\Gamma##.
 
  • #12
63
13
Neither ΓΓ nor the BiBi include axioms, as they are of a different kind. Axioms build the framework, or calculus, or setup of what follows. They have to be minimal in number and without contradictions. This is not true for Γ.Γ. If False ∈Γ False ∈Γ, then we still can get a valid proof. Indeed it happens regularly in mathematics, that a conclusion is drawn without bothering existence!
For someone to give guidance to the person asking the question, they need to know Mendelson's book, the book must be on the table before. The detail shown is not enough. I have the book, not the English edition, and the symbols used are slightly different. I checked what it was about.

Development of the formal theory of Proposition calculus, so when deciding the correctness of a statement is not based on the truth table, but the valid statements are purely linguistic means proven from the axioms.

I wrote this only because the hypotheses as mentioned earlier included "False" as an example. But whoever sees the context of the question will know that this is not appropriate here because the book speaks of a purely syntax-based formal language system, where truth, falsehood does not exist. This is the question of interpretation. But obviously, without the book, you can't see the context.
 
  • #13
stevendaryl
Staff Emeritus
Science Advisor
Insights Author
8,401
2,581
Neither ##\Gamma## nor the ##\mathscr{B}_i## include axioms, as they are of a different kind.
The quote from the first post said that ##\mathscr{B}_i## is either an axiom, or an element of ##\Gamma## or follows from previous statements by the rules of inference.
 
  • #14
13,574
10,691
The quote from the first post said that ##\mathscr{B}_i## is either an axiom, or an element of ##\Gamma## or follows from previous statements by the rules of inference.
Right. This means that the ##\mathscr{B}_i## can be any intermediate step, but ##\Gamma## is still the set which lists the conditions given for a proof. We don't write proofs like: Given ZFC then Zorn's Lemma and AC are equivalent. or even list ZFC in the list of conditions. We separate it into our general framework and only say: Zorn's Lemma and AC are equivalent.
 

Related Threads on Well-formed Formulas Set in Formal Theory

  • Last Post
Replies
2
Views
3K
  • Last Post
Replies
4
Views
1K
Replies
10
Views
908
Replies
3
Views
877
Replies
1
Views
732
Replies
16
Views
4K
  • Last Post
Replies
9
Views
2K
  • Last Post
Replies
1
Views
2K
  • Last Post
Replies
14
Views
3K
Top