Talk:First-order logic
From Academic Kids
In adding a title at the beginning of Talk:First-order predicate calculus (section), I ended up with an extra edit link, one to this part (which was blank). I am making it not be blank, and perhaps this is a good place to capture some ideas about overall organization of the article (and it's Talk).--Orcmid 16:51, 20 Mar 2004 (UTC)
| Contents |
Introductory Material
The introductory statement
- Nevertheless, first-order logic is strong enough to formalize all of set theory and thereby virtually all of mathematics. It is the classical logical theory underlying mathematics. It is a stronger theory than sentential logic, but a weaker theory than arithmetic, set theory, or Second-order logic.
is contradictory for beginners. The statement is made that first-order logic is strong enough to formalize all of set theory, and then it is said that FOL is a weaker theory than ... set theory ... .
The first part of the statement should, perhaps, not be made, and the relationship of FOL to set theory detailed later (along with FOL with =, the formalization of Peano Arithmetic, etc., if one wants to tie those in. And then there is the appropriate tie-in with propositional logic. --Orcmid 16:47, 20 Mar 2004 (UTC)
I also think the statement
- Like any logical theory, first-order calculus consists of ...
is too off-hand. "Like any logical theory" is misleading, I would say. I think we are speaking of how FOL is a formalization of logic. I am not sure how to do that without getting in too deep about what constitutes formalization. But even a brief sketch, as in these introductory passages, should somehow flow into any extended treatment and not be over-generalized. Does anyone have strong ideas about this? --Orcmid 16:47, 20 Mar 2004 (UTC)
I think that it is time for more scrubbing. There may be too many tacit assumptions in some of the explanation of notation and illustrative applications. And I am not sure the Peano Induction scheme comes off very well, mostly because it requires P(x) to be a schematic term for a formula, and that is not the usual approach. It doesn't seem to allow P to stand for a primitive predicate (literal predicate symbol) of the applied system, for example, and it is perhaps too generous in its allowance of non-logical formulae. --Orcmid 16:47, 20 Mar 2004 (UTC)
Notation
I just changed some of the notation used in this entry and I feel I should justify myself. I changed two things.
Previous version:
- ∀ x ∀ y : (x < y) ⇒ (y > x)
- ∀ x ∃ y : y > x
Current version:
- ∀ x : ∀ y : (x < y) ⇒ (y > x)
- ∀ x : ∃ y : y > x
A mathematician would say I added extra colons. A grammatician would say the previous version elided some colons.
Omitting the extra colons is very common practice, but considering the audience I think the more explicit notation is better. The punctuation is a nice visual cue to the structure of the language. It suggests pluggability. Also, in some cases, not having the colon can lead to serious semantic mistakes when trying to translate the symbols into English (see below).
Hofstadter never elides colons in GEB, which is written for raw beginners.
Transliteration
Previous version of article:
- ∃ y ∀ x : y > x
- (ie: thereExists y forAll x suchThat y greaterThan x )
Current version:
- ∃ y : ∀ x : y > x
- (ie: thereExists y suchThat forAll x, y isGreaterThan x )
Previous version:
- ∀ x : x * 0=0
- ie: forAll x suchThat x * 0=0
Current version:
- ∀ x : x * 0=0
- ie: forAll x, x * 0=0
In both cases, I think the previous version is clearly broken. In English, "such that" only makes sense after "there exists". It makes no sense after "for all".
So the English-speaking mind parses "thereExists y forAll x suchThat y greaterThan x" as something like "There exists some y, for any given x, such that y is greater than x." In symbols, ∀ x : ∃ y : y>x.
(I guess it could be argued that the problem is trying to transliterate math to English symbol-by-symbol in the first place, but I'll pass on that argument.)
-- Jorend
History
When did predicate calculus first appear?
Who first devised/used it?
Why?
What were its precursors?
Conditional
This is symantec, but important to help garner respect for Wikipedia: modern logic uses →, rather than ⇒ as its conditional within WFFs.
- Not true, both forms are widely used. The most established symbol for implication is still the most used by philosophers:
<math>\supset<math>
- It would be good to have a default standard specifying symbols for logical connectives. ---- Charles Stewart 17:45, 15 Sep 2004 (UTC)
Definition of first-order calculus is wrong
A recent post by Sandy Hodges on the FOM list [1] (http://www.cs.nyu.edu/pipermail/fom/2004-August/008477.html) points out that the way first-order calculus is specified on this page is wrong for almost all commonly used formalisations of FOL, because the rule of generalisation, simply read, does not take theorems to theorems. The rule needs correction. I plan to have a go in the next few days. ---- Charles Stewart 17:53, 15 Sep 2004 (UTC)
Of course, I'm running horribly behind with all my logic editing plans.
Refining terminology
- (first-order logic) is a stronger theory than sentential logic
This statement is true only if we assume that sentential logic is zeroeth order; this ignores the existence of second-order propositional logic, which is a much stronger theory than first-order predicate logic.
I think that we need a more careful and consistent terminology across the mathematical logic pages when referring to logical systems and calculi, and also we need a common place to talk about the many conventions we have in the logic pages. I mentioned the idea of a Wikiproject for logic in the Talk:Logic pages, but received a less than heartfelt agreement. I'd like to propose the idea again. ---- Charles Stewart 06:28, 13 Oct 2004 (UTC)
- I've the beginnings of a User:Chalst/WikiProject Logic proposal; comments and suggestions welcome. ---- Charles Stewart 07:29, 13 Oct 2004 (UTC)
Why is this page so math oriented?
I think you guys are doing this page a serious disservice in using only mathematical examples. Maybe you should have a separate page for predicate logic and a seperate page for first-order predicate calculas, the first can be more the philosophy of logic and the latter can be used for math. Or maybe you can just used the current page and expand the scope quite a bit with more standard, non-mathematical, examples.
Thanks for allowing my comment.
- I think quantification is the right place for more philosophical discussion of predicate logic. I think, though, that predicate logic should be a more superficial page mostly concerned with linking to the more technically formal and/or philosophical pages, especially since FOL is not the only predicate logic.
- Since the name has come up, shouldn't this page be called First-order logic, on the grounds that (i) this and its abbreviation FOL are the terms I most commonly encounter for the logic, and (ii) FOPC is a misnomer in any case, since there is no consensus what"calculus" should be associated with the consequence relation, the Hilbert-Ackermann formulation being only the most commonly cited. ---- Charles Stewart 11:54, 13 Feb 2005 (UTC)
- Yes, it should be moved to First-order logic. Nortexoid 00:54, 22 Mar 2005 (UTC)
Peano Axioms?
The axioms are non-logical -- i.e., they are not valid in the predicate calculus (hence the name 'non-logical'). PA is just one first-order theory and should not be included in this article at all. Link it. I have a very strong urge to remove it, but I will wait for some comments. Nortexoid 08:44, 23 Mar 2005 (UTC)
IE6 symbol changes
I don't believe there's a policy on this, but it's my humble opinion that since nearly all our readers use IE6, we shouldn't use symbols that IE6 can't render, such as ∀, ∃, ∧, and ∨. Instead, use <math> tags. I know it's not pretty, but it's a lot more readable than funny boxes. Deco 04:07, 26 Mar 2005 (UTC)
- IE can render those symbols -- i.e. unicode. If it doesn't, I'm not sure what the cause of the problem is.
- Also regarding the min. number of operator symbols, I think it's 2, not 3. Perhaps that is only for propositional logic, as I cannot recall how one quantifier would be defined in terms of the other using a Scheffer stroke. I don't have my resources on-hand to check. Nortexoid 05:01, 26 Mar 2005 (UTC)
Some comments, mostly in response to comments & edits of Nortexoid
I'll just dive in:
- The axiomatisation of arithmetic, and hence the Peano rules is of particular interest to FOL, because the intended theory is usually understood to be beyond the ability of FOL to axiomatise (depends on how your read the incompleteness theorems), its the simplest such theorym and hence the "limits of FOL" section this article ought to have would best treat arithmetic.
- Yes, first-order arithmetic is very interesting indeed, but does it merit an entire section in an encyclopedic article on FOL (and when it has its own article)? I still find it best to place a link, perhaps in the Metalogical theorems section that states that FOL cannot provide an axiomatization of arithmetic, linking to the appropriate corresponding articles. Nortexoid 10:46, 26 Mar 2005 (UTC)
- There is such a thing as higher-order propositional logic (ie. there are higher-order theories, of which the simplest is System F, that do not have quantification over individuals, hence no predicates, but only over propositions).
- I wasn't aware of that. However, in a previous edit, it was stated that just plain old propositional logic (i.e. classical propositional logic) was of higher order than predicate logic. Hence my editing comment. Nortexoid 10:46, 26 Mar 2005 (UTC)
- Do we have a consensus for a move to First-order logic? I proposed the move earlier, and Nortexoid agreed.
Although I still don't like the treatment of generalisation, I'm generally happy with the recent edits on this article. Good work! --- Charles Stewart 08:17, 26 Mar 2005 (UTC)
- My hand is still raised. Nortexoid 10:46, 26 Mar 2005 (UTC)
- I agree with the name change to first-order logic. Deco 02:39, 1 Apr 2005 (UTC)
Undecidability of FOL
I just noticed an edit in the Metalogical theorems section that refers readers to Gödel's incompleteness theorem in regards to the undecidability of FOL. That is misleading. Results conerning the undecidability of FOL come from Church, while Godel's theorem conerns specifically arithmetical theories of FOL, like Russell and Whitehead's (or generally N, or PA), and not FOL generally. That is, Godel's theorem is not a result about FOL generally. Nortexoid 03:11, 27 Mar 2005 (UTC)
- My mistake — you're right. Deco 04:45, 31 Mar 2005 (UTC)
FOL set theory comparison
I don't understand "first-order logic is strong enough to formalize all of set theory", yet fol is "weaker than" set theory. Can someone clarify?
- I noticed this also. The first part is quite correct, the "weaker than" part I think is false, unless they mean it in some weird sense I don't get. Deco 04:45, 31 Mar 2005 (UTC)
- It's ambiguous or incorrect. I suppose what is meant is that while FOL is capable of formalizing set theory, any axiomatization of set theory using countably many axioms in FOL is unable to fully capture set-theoretical concepts like set, countable, correspondence relationships, etc. This is a result of the so-called "Skolem's paradox". In any case, if one isn't familiar with certan metalogical results of FOL, then that paragraph is obviously confusing, and it gives no explanation or lead as to what it means. It is probably better removed. Nortexoid 00:36, 1 Apr 2005 (UTC)
- Sorry, that sentence actually makes complete sense now that I reread it. It's strong enough to formalize e.g. arithmetic but it is weaker than arithmetic since it cannot prove certain arithmetical truths. All classical tautologies will belong to a theory arithmetic plus a set of arithmetical truths not provable in FOL without some set of arithmetical axioms (in which case it becomes a theory of arithmetic). If the sentence is put back into the article it should be explained. Nortexoid 01:26, 2 Apr 2005 (UTC)
Interference between treatments of propositional and predicate logic
At present, this article introduces the calculus by layering it upon the definition of propositional calculus:
- The predicate calculus is an extension of the propositional calculus. If the propositional calculus is defined with eleven axioms and one inference rule (modus ponens), not counting some auxiliary laws for the logical equivalence operator, then the predicate calculus can be defined by appending four additional axioms and one additional inference rule.
This definition appears to assume that the propositional calculus is given in a Hilbert-style, whereas the calculus is given in natural deduction style (esp. no axioms, only rules). Natural deduction makes the rule of universal generalisation problematic: the rule is valid only if it is interpreted as making restrictions on open assumptions, which inexperienced users of the logic are unlikely to grasp.
I suggest we change this article to formulate the calculus in natural deduction, for example as is done in the Stanford Enclyclopedia of Philosophy article (I added the link). An alternative would be to create a page documenting propositional logic in a Hilbert style and build on that. Perhaps we should do both. --- Charles Stewart 16:25, 20 May 2005 (UTC)
First-order logic versus Mathematical logic
Most of the content of Mathematical logic is about First order logic, which is not surprising given the universality and historical development of logic. But we should decide where to put what. Perhaps mathamtical logic should be about standard results in first order logic, which is now mostly the case. First-order logic should point to Mathematical logic, and discuss the differences with other logics. vkuncak, Sun Jun 19 11:04:38 EDT 2005
