Talk:First-order logic/Archive 1

FPC

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)

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)

I am trying to understand the paragraph including the '∀x φ', and the explanation, read as: 'for all x, φ'. It is not explained what x is, and what it's relationship to φ means. Is, for instance, x a word in the sentence φ? I am trying to understand a given statement that 'Prolog is based FOC', yet I am finding this article very hard to understand --Benclewett 14:37, 10 April 2007 (UTC)

Comparison with HOL

I am confused by the comparisson with HOL. First, what are properties? (Are they properties of the variables and terms that are introduced with FOL?). Second, the sentence "...i.e. it cannot express statements such as "for every property P, it is the case that...", which nearly suggests that FOL can't quantify but quantifiers have just been introduced. I added a link to 'Property'. -- [[1]] 17:03, 27 Oct 2005 (LMT)

Sentence "can not quantify over PROPERTIES" should really be "can not quantify over PREDICATES". This is a misleading understatement. A reader might get an idea that FOL only deals with unary predicates... thus reduces FOL to [monadic logic] which is actually decidable!

Why should we substitute 'predicates' for 'properties' in that sentence? When we speak of quantification in FOL we are speaking about quantification over individuals, not the variables that denote individuals. We can just as well speak of HOL as quantifying over properties, not the predicate variables that denote properties. Nortexoid 19:11, 24 December 2005 (UTC)

I think we should use predicates instead of properties because it is a more general term. Also - I think that predicate variables denote predicates - not propreties. --Zlimarcelix 14:59, 25 December 2005 (UTC)

The term isn't more general. In FOL predicates are taken to denote properties--i.e. sets of n-tuples of the domain, while the predicates are just symbols of the language. The distinction between predicate and property is one between syntax and semantics. In HOL individual variables range over individuals of the domain while predicate variables of n arity range over sets of n-tuples of the domain--that is, they range over properties. It is true that the predicate variables are bound, but we do not say that there is quantification over predicates, we say there is quantification over properties.

Henkin in Completeness in the theory of types says, "By a valid argument of the second order calculus is meant one which expresses a true proposition whenever the individual variables are interpreted as ranging over an (arbitrary) domain of elements while the functional variables of degree n range over all sets of n-tuples of individuals. Nortexoid 21:29, 25 December 2005 (UTC)

I agree (syntax&semantics)... So - I guess property can denote n-ary relation too? Certainly where I'm from we don't use the term in that way (I'm not a native english speaker). --Zlimarcelix 08:13, 27 December 2005 (UTC)

They're called relational properties. In logic we equate sets, i.e. the extensions of predicates, with properties. In philosophy more generally we don't; or at least what is called a genuine property is monadic and distinct from a relation. Nortexoid 21:17, 28 December 2005 (UTC)

There is a better statement in HOL page: "in first-order logic, roughly speaking, it is forbidden to quantify over predicates". Informal enough - and not misleading. --Zlimarcelix 12:28, 24 December 2005 (UTC)

FOL does quantify over predicates of zero arity, so that statement is inaccurate. Nortexoid 19:11, 24 December 2005 (UTC)

Can you please explain this last one - "FOL does quantify over predicates of zero arity"? As I understand you are saying that FOL quantifies over propositions. It does not. Anyway - what bothers me is this implicit "predicates are really just properties" present in introduction. Am I the only one? --Zlimarcelix 14:59, 25 December 2005 (UTC)

What I wrote makes no sense. I'm not sure what I was thinking at the time. Nortexoid 21:29, 25 December 2005 (UTC)

What is a Predicate

I've trawled Wikipedia, and I still don't know what a predicate is. Well, actually, I'm almost sure that I do, but no thanks to this article. I'm only beginning to really grok this stuff, and not to have a clear, concise definition of 'predicate' in any of the pages dealing with predicate logic (no matter what you call it) is soooooooooooooooooo FRUSTRATING. Go on, I know you don't believe me, it has to be defined somewhere, right? Nope.

This is a bona-fide hole in the logic pages. I'll put starting this article on my tasks list. --- Charles Stewart 15:37, 27 October 2005 (UTC)

I think that "predicate" (in intro section) should point directly to predicates in mathematical logic - where it says "In predicate logic, a predicate can take the role as either a property or a relation between entities" which is OK. --Zlimarcelix 12:16, 24 December 2005 (UTC)

Hi,

A predicate is simply that which is asserted or denied of the subject of a sentence. e.g. Fx - x is red. Here the predicate is 'is red'. I am asserting that this predicate is true of x. Frank Carmody 17:03, 15 January 2006 (UTC)

Grammar

The use of the letters of the Greek alphabet is not defined. I must assume they are propositions from the propositional calculus (and stand for complete propositions), whereas the remainder of the grammar defines the notation for the new constants, variables and functions. Could someone verify this?--[[2]]

An emerging convention is that Greek letters are metalogical devices whose first job is to reduce (not eliminate--nothing can achieve that!) use-mention confusions. Once this is established, you don't need Quine corners or to enclose all sorts of expressions in fastidous single quotes. If the entry intends this usage, it should say so explicitly. A recent text that makes heavy metalogical use of Greek letters is Bostock (1997).202.36.179.65 20:20, 31 March 2006 (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.

In any standard textbook on (mathematical) logic, colons are not part of the language and so they should not be used in formulas. The only time colons and dots are used is as a replacement for parentheses. The colons look ridiculous---they do not add anything to the (unique) readability of formulas. Nortexoid 19:16, 24 December 2005 (UTC)

I certainly have no problem with that; I just used the notation I found. My favorite approach is $(\forall x.\phi )$ and $(\exists x.\phi )$; I think that scope is so important that explicit parentheses are justified. Randall Holmes 22:27, 3 January 2006 (UTC)

I would suggest $(\forall x)\phi$ and $(\forall x)(A(x_{1},\dots ,x_{n})\dots )$ to exclude any symbols that are not part of the language. If we use parentheses, dots and colons aren't needed. Nortexoid 01:02, 5 January 2006 (UTC)

I'm not about to engage in an editing war about this, but the definition of equality which I gave as an example would benefit from a dot after the quantifier; the repeated P is distracting. As I said, in my own writing I never omit parentheses or an intermediate dot where quantifiers are concerned, though this is a matter of taste... Randall Holmes 03:29, 5 January 2006 (UTC)

For improved readability simply place each quantifier and associated variable in parentheses, and enclose the matrix in parentheses as well--e.g. $(\forall x)(\forall y)(x=y)$. This is probably the most common practice (in conjunction with using brackets [,], and braces {, }). It's not a big deal but I'm opposed to using notation within the object language that is not officially part of the object language. I also prefer to keep the primitive notation at a minimum. Nortexoid 05:36, 5 January 2006 (UTC)

That works (the result is readable) but it should be noted that there is no strictly correct notation here: there are variants which appear in the published literature. For example, referees read my $(\forall x.\phi )$ without difficulty (and that is how I specify a well-formed universal quantifier sentence when I present a grammar for first-order logic, which I do from time to time). All that is necessary is that the grammar in use in any given text be clearly specified (particularly if it is not standard). That said, I have no objection to Nortexoid's favored grammar -- particularly given permission to add parentheses for clarity. Randall Holmes 06:19, 5 January 2006 (UTC)

Agreed. The object language, if it includes quantifiers of time-honored form, should include a way of demarcating scope. I use square brackets, reserving parens for resolving ambiguities arising from infix connectives.

It is insufficiently appreciated that the notation of FOL can be greatly streamlined as follows. Let:

1. One of conjunction or disjunction interpret concatenation of atomic sentences;
2. Negation interpret enclosure in parens or some other style of brackets. You now have an expressively adequate set of connectives;
3. All variables be universally quantified by default. Let ∃xFx interpret (x(Fx));
4. a∈b interpret ab. You now have enough notation for set theory;
5. a=b interpret Iab, but I am open to suggestions here. In any event, you now have FOL with identity.

Charles Peirce proposed in 1902 a notation very similar to (1)-(3) above. Jay Zeman had related ideas in a 1967 JSL paper. Around 1961, Brad Angell devised a way of notating all of FOL using just '(' and ')'. This should come as no surprise to anyone knowing the rudiments of computer engineering, because as we all know, computers reduce overything to strings of 0s and 1s.202.36.179.65 08:46, 1 April 2006 (UTC)

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:

1. ∀ x : x * 0=0
   • ie: forAll x suchThat x * 0=0

Current version:

1. ∀ 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?

It's "in" Principia but buried under an avalanche of symbolism and other notions, such as the theory of types. A full awareness of the centrality of FOL had to await Principles of Theoretical Logic by Hilbert and Wilhelm Ackermann (1928). The predicate calculus is very clear in Willard Quine's 1940 Mathematical Logic and Alonzo Church's 1944 Introduction to Mathematical Logic.

That FOL was very important was evident as soon as it became clear that ZFC, Peano arithmetic, and nearly all algebraic structures could be formulated as first order theories (if FOL admits axiom schemata), although I am unsure how this realization came about. Tarski formulated high school algebra and Euclidean geometry as first order theories around 1930, although did not publish this result until 1948.

Who first devised/used it?

Frege in his 1879 Begriffsschrift, which did not clearly demarkate first from higher order logic.

In complete ignorance of Frege, Charles Peirce's student Oscar Mitchell and Peirce himself, discovered quantification 1882-85. This work culminated in a classic 1885 article by Peirce alone, which does demarcate first from higher order logic. Frege's notation is utterly weird and was never taken up by any one else; the Peirce-Mitchell notation closely resembles that used today, and was that of Leopold Loewenheim, Skolem, many Polish logicians, and even Kurt Goedel (1931).

Why?

To formalize the foundations of mathematics. That predicate letters and quantified variables might be a powerful way of reasoning about natural languages emerged in the work of Carnap, Henry Hiz, Noam Chomsky, and Chomsky's teachers, Zellig Harris and Richard Milton Martin.

What were its precursors?

Frege's precursors are poorly understood; see Hans Sluga's 1980 monograph. There is also no biography of Frege. Peirce's road to quantification, on the other hand, has been scrutinized; see Geraldine Brady's 2000 monograph, who highlights, among other things, Peirce's fascination with Augustus DeMorgan's pioneering work on relations.202.36.179.65 09:28, 1 April 2006 (UTC)

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:

$\supset$

It would be good to have a default standard specifying symbols for logical connectives. ---- Charles Stewart 17:45, 15 Sep 2004 (UTC)

• JA: No, the variation in calculi across different communties of usage will likely remain recalcitrant to standardization, for the following reasons. It is not just a matter of using different symbols for the same thing, but in fact reflects what is very probably an irreconcilable difference in underlying philosophy of notation. Many logicians trained in philosophy departments, following the Frege-Russell-Quine tradition, consider the difference between "->" and "=>" to be the moral equivalent — and decidedly not the moral biconditional — of the all-imporatnt distinction between use and mention. Whereas folks who learn their logic largely in passing while proving theorems in mathematics think that that's a distinction without a w(h)it of a practical difference, and would gloss it over under the general semantic umbrella of how it is that terms and expressions denote mathematical objects in the first place. So the math users feel safe in saving the "->" for functional notation, and always use "=>" for logical implication. On the same score, math folk freely interchange the terms "implication" and "if-then", a thing that I have seen philosophy profs quite literally shudder at. Jon Awbrey 15:14, 9 February 2006 (UTC)

This is a bit of an oversimplification. For example, in categorical logic, "=>" is used for functional notation, because "->" is normally used to express morphisms. Using arrows to express function spaces is not universal; often superscripts are used (because of the parallelism with exponentiation). --- Charles Stewart^(talk) 19:03, 9 February 2006 (UTC)

• JA: Yes, I am rather familiar with that whole ball of wax. I studied categorical logic with John Gray in Chambana back in '84 when CCC's (no, not the tree-planting corps) were still in their preprint diapers. As a rule, though, isomorphisms have to be constructed or proved and not just swept under the rug of notation. But of course you know that. Jon Awbrey 19:20, 9 February 2006 (UTC)

• Not quite at the preprint stage: Lambek's "Functional Completeness of Cartesian Categories" dates back to 1974, and Goldblatt's "Topoi" book was published in 1979. But you've had a good teacher. Actually I failed to make the point that my above edit was about: just because there is confusion in the literature about these things doesn't mean there can't be clarity here. I'd like to begin the task of putting together a style guide for logic articles. --- Charles Stewart^(talk) 19:46, 9 February 2006 (UTC)

• JA: Just the way I remember it, you understand, but there was a sheaf (oh, never mind) of something old from Kinko's, stuff that had long gone out of print, plus a preprint of somethings new from Plotkin and Soare, and I know (what did I know?) there was a general sense of excitement that some sort of 3-ple correspondence or other was just now being pushed through to general satisfaction. Then again, maybe it's just that mathematical subjects spend so much longer in 2-apers than human subjects do. Jon Awbrey 20:00, 9 February 2006 (UTC)

→, introduced by Hilbert and Ackermann in 1928, is now quite standard; even Quine adopted it in the 4th and final edition of his Methods of Logic. I have seen ⇒ employed metalogically, which strikes me as sensible. I have almost never seen it used logically, a practice I frown upon. I employ ⇐⇒ as a metalinguistic infix sign denoting the logical equivalence of formulae expressed in differing notations. We probably owe the horseshoe, $\supset$, along with so much else, to Peano; Principia definitely made it canonical for several generations. It seems to have largely vanished from math logic; I am rather surprised to read that it remains popular in philosophical logic. I do not like it because it invites confusion between FOL and set theory, subjects that, however wonderful individually, must be carefully distinguished.202.36.179.65 19:58, 30 March 2006 (UTC)

Definition of first-order calculus is wrong

A recent post by Sandy Hodges on the FOM list [3] 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)

You fellows have discovered the fault line dividing mathematical logic from philosophical logic. While logic has a splendid philosophical heritage, nearly all of the founders of modern formal logic were mathematicians (or in the case of Bertrand Russell, wannabe mathies). Hilbert and Ackermann, the first to lay down the FOL consensus, were emphatically mathematicians. The first philosophical logician was, perhaps Charles Peirce, followed by Clarence I Lewis. Modern logic was dominated by mathematicians until the revival of modal logic associated with Saul Kripke and Ruth Marcus. This led to an explosion of nonclassical logics and to the creation of the Journal of Philosophical Logic around 1970. Logic can now be exposited making no mention of math, and the mathematician Wilfred Hodges wrote a nice Penguin paperback doing just that. Meanwhile, mathematicians have largely moved away from the study of proof mechanics and foundational issues. Even Godel's theorem is unnecessarily mathematical, because it is hopelessly bound up with Peano arithmetic. Smullyan argues that Tarski's theorem is much more broadly applicable and hence more philosophically relevant, and easier to prove.202.36.179.65 18:53, 30 March 2006 (UTC)

I agree with everything you said User above me, BUT, mathematics is just an extension of philosophy, call it an offshoot domain. So we always get back to step uno. —The preceding unsigned comment was added by Xasthuresque (talk • contribs) 02:03, 15 March 2007 (UTC1)

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)

Very much agreed.202.36.179.65 18:55, 30 March 2006 (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)

Regarding IE and symbols, perhaps the meta-equiv tag for "Content-Type" and charset="UTF-8" causes the problem. -anon

Some comments, mostly in response to comments & edits of Nortexoid

I'll just dive in:

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

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

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

It's correct. In FOL, we can formalize all of set theory, that's we can put for example, all axioms of ZF or ZFC (or any other formulation of set theory such as MK, BNG, ...), and work with it. FOL is weaker than set theory, cuz these axioms are not theorems in FOL. ("Mathematical Logic", by Mendelson, chapter 4, "Set Theory" by Konen) Some logician say that Second Order logic is just FOL plus ZF. rdt 11 Nov 2005

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)

My preferred approach to FOL is via semantic tableaux; see the classic text by Richard Jeffrey, and David Bostock (1997). Problem: it is hard to typeset. If that objection is treated as fatal, the propositional calculus (better, sentential) should be set out in the natural deduction style.202.36.179.65 19:02, 30 March 2006 (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

I'd say that any logic that is not, in principle at least, first-orderisable has a dubious claim to being mathematical logic. But there are some tricky caveats about that: is modal logic first-orderisable? What about important non-first-orderisable logics that have played an important role (and indeed continue to play) in the development of ML? I'm not quite sure what I would want to write in fulfilment of your request. --- Charles Stewart 15:34, 27 October 2005 (UTC)

difficult for topology?

the intro says that it is difficult to use first order logic to formulate topology, but never really expands on that in the article. is it because the domain of discource in topology usually includes (quantification over) sets (of points) and not just points? -Lethe | Talk 20:47, August 7, 2005 (UTC)

This statement confuses me, too, and I was a topologist at one time. Topology needs set theory, but set theory in a first-order framework is adequate. Randall Holmes 15:58, 27 December 2005 (UTC)

I'm going to see if I can figure out who wrote that and ask. -lethe ^talk 16:27, 27 December 2005 (UTC)

It was 128.2.70.48 t c. A CMU address. Made a few dozen edits in May 2004. Mostly minor, a few contributions of mathematical content which seem to be correct. I doubt if he's watching his talk page though. I'm inclined to remove it, as it doesn't seem true to me, I'd want a source. -lethe ^talk 16:50, 27 December 2005 (UTC)

Agreed. If (a) topology can be formulated in ZFC, and (b) ZFC is a first order theory, then (c) topology is likewise a first order theory.202.36.179.65 19:06, 30 March 2006 (UTC)

confused

I'm confused... starting with the "peano axioms are not valid". Does that mean that in a "valid" predicate calculus, all axioms must be in the form of the 4 axiom schemas? And set theory can be put in this form, but peano axioms cannot? There are no predicates with 2 parameters in the schemea, which would disallow things like a "equals" predicate.

Perhaps a example of a valid (and trivial) extention of predicate calculus, (and maybe a example of a invalid (and trivial) one too)

Also, if resolution is refutation complete, then how do we not have a decision procedure for first order predicate calculus?

• Where does it say any of these things? The only notion of "valid" I am familiar with is the validity of a formula; for example, (Ax) (Ay)[x=y => y=x] is valid, but (Ax)(Ay)[x=y] is not, since it fails in any model with more than one element. The refutation completeness of resolution allows the theorems of FOPC to enumerated, but it may take an arbitrarily long time for the refutation to be generated, so there is no point at which one can conclude that a statement is not a theorem. User:Ben Standeven at 70.249.214.16 02:04, 14 October 2005 (UTC)

rewrote blurb, corrected errors

I rewrote the introductory section, which I found really muddy; I think I preserved all the links that are needed.

I corrected mistakes in several places in the balance of the article. I removed the assertion that the Peano axioms are not valid for first-order logic (correct but confusing). I removed the incorrect definition of atomic sentence (all sentences P(t_1,...,t_n) are atomic; it has nothing to do with arity of P). I dealt with the inconsistency between the statement that modus ponens is the only inference rule and the additional (necessary) provision of universal generalization as an inference rule. The axioms are (I think) correct, but it is not adequate to construe W and Z as predicate letters: the correct statement of how W and Z are to be understood is supplied. Have a happy holiday season. Randall Holmes 17:10, 27 December 2005 (UTC)

Proposal to merge Predicate Calculus article into this one

In my experience, when people say "(the) predicate calculus" they almost always mean (classical) first order logic. I followed a predicate calculus link expecting to find a nice, detailed article on FOL and instead found this stumpy, pathetic little article with unorthodox notation that I doubt many people would find helpful at all. Dbtfz 06:22, 19 January 2006 (UTC)

• JA: Quality of the article aside, in my acquaintance many people would include "higher order predicate calculus" (HOPC) under PC, but not of course under FOL. Jon Awbrey 06:34, 19 January 2006 (UTC)

• I would redirect "predicate calculus" to FOL and discard the existing predicate calculus article. Randall Holmes 13:15, 19 January 2006 (UTC)
  • I would be amenable to either solution. Redirect to FOL per Randall, or make an article about HOPC there per Jon (but let's have that redirect in the mean time). -lethe ^{talk +} 02:03, 31 January 2006 (UTC)

It would be a good idea to seek out Charles Stewart's opinion on this. Paul August ☎ 02:51, 31 January 2006 (UTC)

I've left Charles a note on his talk page. Paul August ☎ 02:58, 31 January 2006 (UTC)

• JA: I'm going to redirect the NP article to the P article, and dispense with the NP article once and for all. Another pleonasty problem solved by indirection, er, redirection. Jon Awbrey 03:16, 31 January 2006 (UTC)

Thanks, Paul. Given the lousy state of the PC article as it stands, turning it into a redirect to this article would immediately improve the coverage we have among the logic articles. I can see a case, along the lines suggested by Jon, for an independent article in summary style on the various alternate predicate calculi (first- vs. higher- order; classical vs. intuitionistic vs. relevance vs ...; generalised quantifiers; pure type systems; categorically inspired logics); however, it's not clear until we have figured out how to put this article together what it is best called: if the most coherent article along these lines takes a diachronic view, then it is maybe best called History of predicate logic. We can see what is best done with such content when we have it. --- Charles Stewart^(talk) 16:25, 31 January 2006 (UTC)

• Paul from VA: The PC article should be kept separate, despite the fact that the PC article does not satisfy the commenter above. Although it is like the fact that you may prefer a full muffin compared to someone who likes to eat only the muffin tops, it does not account for the appetite of the person that is hungry. In other words, not merging the PC article provides a better capacity for a person to handle the cognitive load of the topic of logic. You don't teach a person calculus without algebra; it is separate because FOL introduces other concepts apart from PC. [UPDATE: I thought you guys were referring to Propositional Calculus; thus, the merge proposal could be correct, my error.]

references to pairing and relation algebra

I added references to the technical possibility of eliminating predicates and functions of arity > 2 if an ordered pair or its projection relations are provided (with suitable axioms). I also added a reference to the equivalence between FOL with the same extension of vocabulary and a natural system of relation algebra with projections of an ordered pair as special relations; I will eventually add an article on this relation algebra. This is from a book by Tarski and Givant, and apparently has excited some interest in CS. Randall Holmes 16:50, 31 January 2006 (UTC)

In complete ignorance of what you wrote above, I created the entry relation algebra! Kalmar (1936) and Quine (1954) proved that all predicates of arity > 2 can be reexpressed using predicates of arity 2. One would like to think this an elegant fact; nevertheless, it has drawn little attention in the literature; good to see you thinking like me. (Peircians argue that Peirce's reduction thesis, proved by Hertzberg in 1981, is a closely related result.) Warning: nearly all of the material in Wikipedia on relations is by one Jon Awbrey.202.36.179.65 19:18, 30 March 2006 (UTC)

First-Order Theory redirect

Intrigued in the topic of FOL, I was curious as to what made this logic different from other types of logic and why it is "first order". While this Article does a great job of answering my first question, it made a meager attempt to describe what a first order theory is by providing a link to an article "first-order theory" and briefly talking about ZFC and axioms. Unfortunately, the link to first-order theory redirected right back to first order logic, leaving me with a few examples of first order theories, but not a very clear definition of what it is. Surely First-Order Theory ahould not redirect to first-order logic if it is not the only theory of this kind. Apparently, ZFC and Peaso Arithmetic are also theories of this kind, so I believe that first-Order theory should have it's own article with a basic overview of what defines a theory of this sort followed by some links to the example theories briefly mentioned in the FOL aricle. Of course, I would write the article myself, but I came here asking the question, not knowing the answer. lokoluis15 69.254.149.179 04:34, 2 March 2006 (UTC)

• edit* After seeing the related links page, I found a more relevant article for the article "First-order theory" to redirect to. I think that this article is much better suited for the job than the FOL article, as it provides a broad overview of first-Order theories, instead of just one example. lokoluis15 69.254.149.179 06:21, 2 March 2006 (UTC)

On the distinction (made by ∃) between connectives ∧ operations

• JA: We'll eventually have to sort out some of the confusion that is currently well-distributed throughout WP logic-related articles over the distinction (that some writers, e.g. Quine, are sticklers about) between connectives, which operate on syntactic thingies, and mathematical operations, which are mathematical objects. The word "operator" is widely used in a way that vacillates between these two poles. Not everybody makes the distinction, but it is necessary to be aware of it in any case. Probably not ready for that just yet, but I do see the day coming. In the meantime, let's all try not to compound the confusion. Jon Awbrey 19:46, 18 March 2006 (UTC)

Typo?

The first bullet point in the Vocabulary section contains the sentence: "The minimum number of primitive symbols needed is one, but if we restrict ourselves to the operators listed above, we need three; for example, ¬, ∧, and ∀ suffice." Should that ∀ be a ∨ for "logical and"? --jivy 03:21, 22 April 2006 (UTC)

Firstly, ∨ stands for logical or. Secondly, no. You can get ∨ from ∧ using ¬ (see de Moivre). You need a quantifier, or else you're not doing first order logic, you're doing sentential logic. So the ∀ definitely cannot be replaced by a ∨, though it can probably be replaced by a ∃. -lethe ^{talk +} 03:33, 22 April 2006 (UTC)

Damn. I think I got de Moivre and de Morgan mixed up. -lethe ^{talk +} 03:35, 22 April 2006 (UTC)

Vacuous statement

The intro states that "it is generally accepted that all of classical mathematics can be formalized in ZFC". Well, yes, since the article Classical mathematics defines this as "mathematics constructed and proved on the basis of classical logic and ZFC set theory". So, given that definition, the claim from the intro reduces to:

It is generally accepted that all mathematics constructed and proved on the basis of classical logic and ZFC set theory can be formalized in ZFC.

The subtext meaning of phrases like "generally accepted" is usually something like: "although contended, widely supported". But here there is nothing to contend, and acceptance is not support; the statement is vacuously true.

Suggestions for an NPOV formulation having substance, and yet standing a chance of being consensual, will be graciously accepted. --Lambiam^Talk 10:01, 3 June 2006 (UTC)

Lambiam, I agree with your point. I propose to change

The usual set theory ZFC is an example of a first-order theory,
and it is generally accepted that all of classical mathematics can be formalized in ZFC.

in

The axiomatic set theory ZFC is a first-order theory,
and it appears in practice that all of mathematics can be formalized in ZFC.

Otto 12:50, 5 August 2006 (UTC)

There's also something fundamentally wrong, though I can't pintpoint it exactly. The trouble is, Peano Arithmetic can *not* be axiomatized in FOL. The last axiom, which says that we are concerned with the smallest set that fulfills the preceding axioms, needs second order logic. So if PA can be "implemented" in ZFC, then ZFC is also not expressible in FOL. Somehow it's wrong. 88.73.225.37 22:54, 4 September 2006 (UTC)

The Peano arithmetic article suggests that the term generally refers to the first-order system, even though Peano originally formulated his induction axiom as second order. 192.75.48.150 17:48, 5 September 2006 (UTC)

Inference Rules

Is there any reason that the names of these rules are not given? Adam Acosta 22:19, 12 July 2006 (UTC)

Valence or arity

The article uses the term valence. Valence has no lemma in this meaning in wikipedia whereas arity has. Therefore I propose to use arity and add valence as another synonym for arity in the article arity. Otto 12:28, 5 August 2006 (UTC)

Confusing Lead

I found that the lead of this article is very confusing and unhelpful for a reader unaware with the topic. Can anyone rewrite it to make it clearer. 202.63.233.8 16:02, 8 August 2006 (UTC)

Technical reference

I moved a abbreviated set of definitions for first order logic from the page mathematical logic to Talk:First-order logic/Technical reference. I don't know if it is helpful here but it wasn't helpful in the other place. The guideline WP:SUBPAGE discourages linking directly from articles to subpages of talk pages, so please move the reference somewhere else before linking to it from an article. CMummert 12:21, 29 October 2006 (UTC)

Density

Is there any way that, well, a layman can understand this article (or at least the introduction and first paragraph) without going link-hunting through all the notation used, or is the subject just that dense? I am, of course, unqualified to do anything about it (if it can be done, or should be, or whatever,) but I was wondering if there could be an introduction for the uneducated. TwilightDragon 01:40, 30 December 2006 (UTC)

Good intro to FOPL

Well, I found it informative and a little more transparent at first glance than this article! I wonder if someone with a grounding in logic might be able to use this? (You might need to scroll down a little to get into the meat of the article. Mark 23:39, 28 January 2007 (UTC)

http://scienceblogs.com/goodmath/2007/01/basics_logic_aka_its_illogical_1.php#more

removed two identities

I removed two of the four identites recently added by an anonymous user, since they are only true for non-empty universes:

$P\land \forall x\,Q(x)\Leftrightarrow \forall x\,(P\land Q(x))$ (where the variable $x$ must not occur free in $P$)

$P\lor \exists x\,Q(x)\Leftrightarrow \exists x\,(P\lor Q(x))$ (where the variable $x$ must not occur free in $P$)

(In an empty universe, the right-hand sides are independent of P whereas the left-hand sides aren't.)

Joriki 07:12, 3 February 2007 (UTC)

Various comments: (1) Those identities are logically valid in the usual quantification theory, which requires models to be non-empty (Mendelson, 1997). Empty universes are not usually considered, because they are seldom interesting, can be easily simulated using an auxiliary predicate in the few cases where they are interesting, and complicate the axiomatization of the resulting notion of logical validity.

(2) Actually it would be well with some prose that informs the unexpected reader what the "Identities" section is about at all − are they to be taken as statements about truth in models, or as proof rules, i.e. logical axioms that just happen to have a biimplication as their topmost connective?

(3) Given that first-order logic can be formalized in many different ways I think we should settle on one particular formalization to reproduce in the article and source it explicitly such as to discourage well-meaning readers from inserting rules from their own favourite system that are superfluous in the context. Otherwise we risk ending up with a massively redundant description that make readers think that the proof theory of FOL is more complex than it is. (In fact, we already have such redundancy, as the "Quantifier axioms" and "Predicate calculus" sections seem to compete for the role of axiomatically characterizing FOL). Henning Makholm 22:47, 3 February 2007 (UTC)

Thanks for the detailed comments.

The assumption of a non-empty domain should be made explicit. There's an article on empty domain, but the articles on quantification, existential quantification and universal quantification neither mention how to interpret the quantifiers in an empty domain, nor make an assumption about non-empty domains.

Another reason for removing the identities I removed, though, would be that in a non-empty domain they follow trivially from the ones above by dropping the dependence of P on x, whereas the two remaining ones only work in one direction if P depends on x (and appear below under "inference rules" in that form).

By the way, the German article at de:Prädikatenlogik also mentions only these two, and the section they're in is entitled "Some equivalences of predicate logic".

Joriki 07:11, 4 February 2007 (UTC)

The article is about classical FOL and so the identities you removed are theorems of FOL. In fact, they are used in the construction of prenex normal forms. Moreover, it is strange that you would remove those for the reason you cite, yet keep other identities that fail in the empty domain, e.g. $P\land \exists x\,Q(x)\Leftrightarrow \exists x\,(P\land Q(x))$ and $P\lor \forall x\,Q(x)\Leftrightarrow \forall x\,(P\lor Q(x))$. In any case, it is not wrong to include them in the article since they are theorems of FOL. Nortexoid 01:49, 5 February 2007 (UTC)

IE and math symbols: more details

Just a heads-up:

The problem with Internet Explorer (and other browsers) not displaying certain math symbols on this page correctly (also mentioned in another post above) is described extensively at Help:Special_characters. Specifically, see the Viewing and Displaying Special Characters sections. The unicode template can be used to force IE into using a font that can display Unicode / UTF-8 characters properly. An alternative is to use ${\displaystyle }$ wikimarkup (see WP:MATH), although this is often avoided, mostly due to the font appearing overly large.

I thought it might be a good idea to "tag" affected articles with the same "Technical note" box displayed at the top of the Help:Special_characters page. At least this will alert affected users about the problem and its cause. If you decide to make use of this, the code is:

<div class="boilerplate metadata" style="background-color: #f3f9ff; margin: 1em 2.5% 0 2.5%; padding: 0 10px; border: 1px solid #aaa;"> '''Technical note''': <small>Due to technical limitations, some [[w:web browser|web browser]]s may not display some '''special characters''' in this article. Such characters may be rendered as boxes, question marks, or other replacement symbols, depending on your browser, operating system, and installed fonts. Even if you have ensured that your browser is interpreting the article as [[w:UTF-8|UTF-8]] encoded and you have installed [[w:List of typefaces#Unicode_fonts|Unicode font]](s) that supports a wide range of [[Unicode]] [[w:Mapping of Unicode characters|blocks]], fonts such as ''[[w:Arial Unicode MS|Arial Unicode MS]]'', ''[[w:Code2000|Code2000]]'', ''[[w:Code2001|Code2001]]'', ''[[w:TITUS (project)|TITUS Cyberbit Basic]]'', ''[[w:Lucida Sans Unicode|Lucida Sans Unicode]]'' or one of the [[w:Free software Unicode fonts|Free software Unicode fonts]], you may still need to use a different browser, as browser capabilities in this regard tend to vary.</small> <includeonly>[[Category:Pages with special characters|{{PAGENAME}}]]</includeonly> </div>

This will display:

—Xhantar^Talk 11:19, 9 February 2007 (UTC)

Question about the definition of a WFF

i I have not seen that definition of a wff. Its how it is used but that is through the idea of completeness. What i have seen is: The set of terms is recursively defined by the following rules:

1. Any constant is a term.
2. Any variable is a term.
3. Any expression f(t₁,...,t_n) of n ≥ 1 arguments (where each argument t_i is a term and f is a function symbol of valence n) is a term.
4. Closure clause: Nothing else is a term.

The set of well-formed formulas (usually called wffs or just formulas) is recursively defined by the following rules:

1. Simple and complex predicates If P is a relation of valence n ≥ 1 and the a_i are terms then P(a₁,...,a_n) is well-formed. If equality is considered part of logic, then (a₁ = a₂) is well formed. All such formulas are said to be atomic.
2. Inductive Clause I: If φ is a wff, then ¬φ is a wff.
3. Inductive Clause II: If φ and ψ are wffs, then (φ → ψ) is a wff.
4. Inductive Clause III: If φ is a wff and x is a variable, then ∀x φ is a wff.
5. Closure Clause: Nothing else is a wff.

This definition is much simpler and easier to read. It does not have the usual binary conectives but they are accounted for by various combinations of ¬ and →; i think that this should also be introduced. I would define free variables separately as well.

1. Atomic formulae If φ is an Atomic formula then x is free in φ if and only if x occurs in φ.
2. Inductive Clause I: x is free in ¬φ if and only if x is free in φ.
3. Inductive Clause II: x is free in (φ → ψ) if and only if x is free in φ or x is free in ψ.
4. Inductive Clause III: x is free in ∀y φ if and only if x is free in φ and xǂy.
5. Closure Clause: if x is not free in φ then it is bound.

I think these revisions will make the definitions simpler, easier to understand. i havent contributed to wikipedia and do not know the polite way to do this :). —The preceding unsigned comment was added by SventhePole (talk • contribs) 20:56, 14 March 2007 (UTC1)

Article Recognition

Coming onto this page with, formally, only a grade-school strength knowledge of the subject, I was able to depart it with a greater understanding of the highly ingroup-intensive subject without any confusion. The page is well organized, verifiable, (subjectively) interesting, and compositionally sound. I believe recognition is in order. .Absolution. 09:17, 23 April 2007 (UTC)