Talk:First-order logic

A question (possible problem?)

In the interpretation section, it seems to me as if the semantics assigned to existential quantification are wrong. It currently states that "a formula \exists x . A is true according to M and μ if there exists an evaluation μ' of the variables only differs from μ regarding the evaluation of x and such that A is true according to the model M and the interpretation μ' " Now in the case of a single entity for which the existential quantification holds, no evaluation μ' would actually exist. Or am I misunderstanding something? —Preceding unsigned comment added by 137.73.9.223 (talk) 13:24, 26 November 2008 (UTC)

How about this?

"a formula \exists x . A is true according to M and μ if there exists an evaluation μ' of the variables, that may only differ from μ regarding the evaluation of x, such that A is true according to the model M and the interpretation μ' "

If that doesn't resolve your question, could you explain another way what you're asking? — Carl (CBM · talk) 13:46, 26 November 2008 (UTC)

Too technical

I'd like to suggest that this article makes no sense to anyone not already familiar with the subject. RobertM525 (talk) 06:55, 15 March 2008 (UTC)

I am familiar with the subject, but I also have my problems with this article. It looks like a huge mess to me, and I think it should be rewritten from scratch. Unfortunately this doesn't have a high priority for me. --Hans Adler (talk) 10:29, 15 March 2008 (UTC)

The article is not too technical, it is as technical as is needed for a mathematical subject. The article is messy and various sections do need rewriting. However, take into account that this is a general article on a large subject-matter. If anyone is interested especifically in proof theory, model theory, etc, they ought to check those articles first. I strongly disagree with the idea of dumbing down the article. --MoisesMB (talk) 10:41, 18 November 2008 (UTC)

I suspect RobertM525 was using "Too technical" in the popular pejorative sense, meaning something like "messy, and needs rewriting", perhaps with the added implication of an inbred style employing needless jargon. If so, then RobertM525 and MoisesMB might agree more than they disagree. --AC (talk) 07:55, 22 April 2009 (UTC)

It is a huge mess with many important missing pieces. The 5 postulates that gover the entire system for instant. P 1. P→P, P 2. (P.Q)→P..... to P 5. (x)P→Q. by Copi Person53 (talk) 06:42, 13 April 2012 (UTC)

There is an entire section on deductive systems. Remember that this is a survey article, not a textbook. There are too many deductive systems to cover them all in detail, so the article simply summarizes them and links to articles that describe them in more depth. — Carl (CBM · talk) 11:17, 13 April 2012 (UTC)

I would suggest that, while the "technical" aspects of the subject need not be dumbed down, a better explanation of the aspect and importance of the subject should be presented for the layperson. There are many references to "first order" logic scattered throughout wikipedia articles on mathematics, computation and the like, and an intelligent layperson would be expected to get a more clear view of the what first-order logic is by clicking to this article. Unfortunately what they get as explanation is not very helpful. Cellmaker (talk) 02:02, 22 November 2012 (UTC)

And this impenetrable sludge is the article after it has already *been* rewritten! Why is it not possible to make at least an introduction to this subject understandable to a layperson? (And I speak as someone who already has an understanding of the subject at university level!)

Nuttyskin (talk) 09:54, 31 March 2023 (UTC)

Proof for Exist x all y P(x,y) => all y exist x P(x,y)

all t P(x,t) => P(x,y) (quantifier axiom)

P(x,y)=> exist z P(z,y) (same quantifier axiom)

all t P(x,t) => exist x P(z,y) (Using prepositional logic tautology for the above two, ((p->z)^(q->r))->(p->r))

all y (all t P(x,t)=> exist z P(z,y)) (Generalizing wrt y)

all t P(x,t) => all y exist z P(z,y) (Using q axiom 3 w= allt P(x,t) z(y)= exist z P(z,y))

all x ( all t P(x,t)=> ally exist z P(z,y)) (Generalizing wrt x)

exist x all t P(x,t) => all y exist z P(z,y) ( Q axiom 4)

exist x all y P(x,y) => all y exist x P(x,y) (changing dummy variables)

Please edit if there are errors and I want to know what is wrong and why.

Thanks

Supems (talk) 17:37, 16 April 2008 (UTC)

I think you mean to prove that: for all y there exist an x such that P(y,x); and the principal mistake is simple (aside from the rest of the confusions and ambiguities). Line 3, P(z,y) is outside the scope of the existential quantifier. There is no x is P(z,y). —Preceding unsigned comment added by Wireless99 (talk • contribs) 17:11, 23 November 2008 (UTC)

Atomic formula

The article uses a notion of "atomic formula", which, however, is not defined.  --Lambiam 23:15, 2 May 2008 (UTC)

The definition is in section Formulas. But the article is an incredible mess and needs to be rewritten completely. It's full of idiosyncracies.

Unfortunately it's another case with a strange mixture of mathematics and philosophy. I can't rewrite the philosophy part because I don't know anything about it. And we don't have experienced philosophical logicians here who could do this. --Hans Adler (talk) 23:32, 2 May 2008 (UTC)

Please Help! (request help in fixing two minor grammatical problems).

There are obvious grammatical problems in the two sentences,

"Monadic second-order logic allows quantification over subsets, or in other words over unary predicates", and

"Second-order logic allows quantification over subsets and relations, or in other words over all predicates."

in the section "Comparison with other logics." I suggest that the problems be fixed by deleting the word "or" in both sentences. Unfortunately, it is possible that my suggestion is incorrect and that one or both sentence should be fixed by deleting "in other words." (The law of the excluded middle applies here - it's one or the other - not both -  :)

However, although I am a student of mathematical logic, I am not an expert in the field. I don't feel sufficiently expert in this field to be able to guarantee that my suggestions yield statements that are cufficiently correct to be useful.

I know we are supposed to be bold, and I try, most of the time, but, this time, I feel that I'm just a little bit over my head.DeaconJohnFairfax (talk) 18:58, 16 July 2008 (UTC)

The problem is not so much of grammar, surely, but of ambiguity of the word "or" is it not. "in other words" implies synonimty so you could say with the same meaning:

"Monadic second-order logic allows quantification over subsets i.e. unary predicates" and ""Second-order logic allows quantification over subsets and relations, i.e. all predicates."

But is "subsets" thus synonmous with "unary predicates" and "subsets and relations" with "predicates"? Is it perhaps more accurate to say "Second-order logic allows quantification over predicate symbols, (monadic second-order logic just in case the predicate symbol is of arrity one.) Under an interpretation a predicate symbol is associated with a set or relation (on the domain). I feel there is a confusion here between "predicate" and "predicate symbol" --Philogo 23:00, 16 July 2008 (UTC)

A 'subset' is a subset _of_ the domain (assuming we're talking model-theoretically, and there's a non-empty set serving as the domain of the interpretation). A predicate symbol of arity one can be _interpreted as_ a subset of the domain, a predicate symbol of arity two can be _interpreted as_ a subset of (domain) x (domain), etc. It's at best bizarre to say that one 'quantifies over a symbol'. The range of the quantifiers (is one of the things that) distinguishes first-order from second- or higher-order logic. (over elements of the domain => first-order or over higher-types => second- or higher-order). Zero sharp (talk) 01:38, 17 July 2008 (UTC)

Subsets are not synonymous with unary predicates, in general. The simplest difference is that predicates have intensional equality, while subsets typically have extensional equality. But predicate variables in second-order logic are virtually the same as set variables - the only difference is syntactic, whether one writes P(x) or x ∈ P

In higher order logic, when one says that the quantifier $\forall X$ quantifies over all subsets of the domain, that means every possible subset, as determined by every possible predicate. This is what the "in other words" in the article is trying to say.

It would be accurate to say that second-order logic allows quantification of predicate variables - the only issue with "predicate symbol" is that it could be used to mean a constant symbol, which cannot be bound by a quantifier. — Carl (CBM · talk) 15:18, 17 July 2008 (UTC)

Yes: my mistake, quantification over predicate variables. But how should we rephase the original sentence distinguishing Monadic second-order logic and (vanilla) Second-order logic?--Philogo 19:41, 17 July 2008 (UTC)

Carl: thanks for pointing out that diff b/w subsets and unary predicates; I hadn't thought of that. The road to hell is indeed paved with good intensions (sic). Zero sharp (talk) 19:44, 17 July 2008 (UTC)

Limitations of first-order logic

The 'limitations' in this section seem to me as if they are shortcomings only to computer scientists; we fault FOL because it doesn't have 'if-then-else' -- why do we not also fault it for not having while-do or a SWITCH statement? I'm not prepared to _Delete_ that section, but I moved it further down (after what I _do_ expect to see listed as a shortcoming: the lack of expressive power - though I think there are more/better examples than finiteness). Zero sharp (talk) 14:53, 30 September 2008 (UTC)

I agree that section is giving undue weight to a very minor issue. But the whole article is in such dire need of revision that I have been ignoring it.

On a related note, the section about countability is somewhat misleading. It is certainly possible to assert in first order logic that every bounded set of real numbers has a least upper bound. Syntactically, anything that can be asserted in second-order logic can be asserted in multisorted first-order logic as well. Indeed real analysis, including the axiom of completeness, is typically formalized in first-order set theory!

What is true is that the semantics of first order logic permit unintended models, so that the sentence asserting the existence of least upper bounds only does so for bounded sets of real numbers in a particular model of the theory at hand. — Carl (CBM · talk) 15:10, 30 September 2008 (UTC)

This is a very trivial sense of 'assert' (or likewise 'express' or 'define'). One would think the appropriate notion is definability w.r.t. a class of models, much in the sense given in the article definable set (but generalized to classes of structures). E.g. this is the standard sense used in modal definability, where a modal formula A defines a frame property P w.r.t. a class C of frames iff for any frame F in C, F validates A iff F has P. Whence []p -> p defines reflexivity (of the accessibility relation governing that modal operator) over the class of all Kripke frames. The same idea is going on in the first-order case when they say that the language (not logic) cannot define or express certain properties. Nortexoid (talk) 12:11, 4 October 2008 (UTC)

I think you mean that a first-order theory of reals permits of unintended models. (Yes, it is true that a first-order language in general does, as e.g. the sentential operators can be interpreted set-theoretically as opposed to truth-functionally, but this is not the usual sense of "unintended model/interpreation".) Nortexoid (talk) 12:11, 4 October 2008 (UTC)

I read "asserts" as a syntactic notion depending only on the intended interpretation of the non-logical symbols in the language. I remember Kleene used the phrase "formulas express propositions" for the same idea. I would argue that no notion of semantics (apart from knowledge of the intended interpretation of the symbols in the formal language) is necessary to determine the natural-language proposition expressed/asserted by a formula. Thus the relationship between the proposition asserted by a formula, on one hand, and the corresponding property that any model of the formula must have, on the other hand, is determined by the semantics underlying the definition of "model of the formula."

From this viewpoint, it doesn't make sense to say that the axioms of a theory permit unintended models, only that the semantics of first-order logic allow these axioms to have unintended models. Because the same set of axioms, if studied in different semantics, may well be categorical (for example, Peano arithmetic). Indeed, trivially, any set of axioms can be made categorical by redefining the semantics so that only one particular model in the previous sense is called a model in the new sense.

For the same reason, I wouldn't say "There are a number of properties not definable in first-order languages....", since there is no syntactic difference between a first-order language and a second-order language (can you tell me whether $\forall A\exists x\,x\in A$ is first- or second-order?). What's true is that there are a number of properties not definable using first-order semantics. This makes perfect sense, since "definable" is a semantic notion, not a syntactic one; but "language" is a syntactic notion. — Carl (CBM · talk) 18:57, 5 October 2008 (UTC)

Importance and applications

Have I missed it or is there no mention at all of the importance and very little of the applications in many fields of first-order logic (as compared with other logics)? Ht686rg90 (talk) 11:30, 9 October 2008 (UTC)

FOL vs Propositional Logic

The argument for why FOL is needed over propositional logic is flawed. The flaw is in the translation from English to propositional logic. The proper translation would be:

• $Socrates\rightarrow Man$
• $Man\rightarrow Mortal$
• $\therefore Socrates\rightarrow Mortal$

A better example is needed for why FOL is more powerful than propositional logic.

Drunkpotato (talk) 20:40, 5 December 2008 (UTC)

Generalized modus ponens

Some time ago, I added Generalized modus ponens to the inference rules (take a look at the link), but it got removed with the explanation "hardly a readable addition and not one of basic inference rules." Admittedly, it isn't very well written. But still, the more information, the better? What do others think? Offliner (talk) 17:13, 15 January 2009 (UTC)

I think "The more information, the better" is a provably false motto, and thus a terrible one to live by (such as in the case of "generalized modus ponens"). Nortexoid (talk) 18:13, 17 January 2009 (UTC)

Why exactly don't you support including it? Offliner (talk) 18:27, 17 January 2009 (UTC)

Plans for significant editing

For a long time I have been thinking this article should be revised. I think I will have some free time in the coming months to work on it. This may involve cutting some of the cruft that has accumulated (like if/then/else) and rearranging the other sections so that the article reads more smoothly. If other people are interested in helping me, please let me know. — Carl (CBM · talk) 18:18, 19 March 2009 (UTC)

This is very good news, I am certainly willing to help. --Hans Adler (talk) 18:50, 19 March 2009 (UTC)

It certainly needs work; trust it will not be re-written soley for mathematicans or model theorists?--Philogo (talk) 22:50, 19 March 2009 (UTC)

No, of course not. The third main group that I think are interested, apart from logicians and model theorists, are computer scientists. I'd like to resolve the "too technical for a general audience" issue. I think that replacing some of the many lists with regular, accessible prose will be a big step. — Carl (CBM · talk) 00:21, 20 March 2009 (UTC)

Logicians, model theorists, and computer scientists are probably the main groups of people interested in the formal treatment of first-order logic. On the other hand, the language of first-order logic is used semi-formally by mathematics in general -- for example, definitions in introductory college-level calculus are very often made precise by symbolic formulas with quantifiers and logical symbols. Students at this level are supposed to develop an "intuitive" understanding of what such formulas mean; they are certainly not subjected to a formal treatment of logic that would work as a basis for foundational work. I fear that the current article is not very helpful to this group of readers, who use FOL symbolism as "the language of rigor" but not as an object of study in its own right. –Henning Makholm (talk) 12:43, 20 March 2009 (UTC)

Good point. That also suggests the article should be more open to multi-sorted languages early on:

∀ ε ∃ δ ∀ x ( d(x,y) < δ → d(fx,fy) < ε)

— Carl (CBM · talk) 13:09, 20 March 2009 (UTC)

Well -- I would personally agree that everyday mathematical reasoning is better modeled by a sorted/typed approach than by the single-sorted universes many formal logic texts work with. But it could be hard to follow that path consistently in the article without getting into tension with core WP editorial principles. The best course might be to sweep the matter under the carpet in the same way mathematics in general does it: Use multi-sorted examples freely early on and then, as quietly as possible, leave them by the wayside when it comes to formal rules. Then, near the end, we can have a brief discussion of the various options for how to formalize "sorted" reasoning. –Henning Makholm (talk) 23:31, 20 March 2009 (UTC)

Logic including first order predicate logic is a compulsory subject for most philosophy students so it should be accessible to them. The use of good clear prose and familiar examples is what's needed IMHO.--Philogo (talk) 00:22, 21 March 2009 (UTC)

I didn't mean to exclude the philosophers; I was lumping them in with the mathematicians. Clear prose is definitely the key. — Carl (CBM · talk) 00:50, 21 March 2009 (UTC)

Clarification

I'm particularly interested on clarification for this section:

" Graph reachability cannot be expressed

Many situations can be modeled as a graph of nodes and directed connections (edges). For example, validating many systems requires showing that a "bad" state cannot be reached from a "good" state, and these interconnections of states can often be modelled as a graph. However, it can be proved that connectedness cannot be fully expressed in predicate logic. In other words, there is no predicate-logic formula φ and R as its only predicate symbol (of arity 2) such that φ holds in an interpretation I if and only if the extension of R in I describes a connected graph: that is, connected graphs cannot be axiomatized.

Note that given a binary relation R encoding a graph, one can describe R in terms of a conjunction of first order formulas, and write a formula φR which is satisfiable if and only if R is connected.[10] "

I can't understand a thing! Does that mean that directed graphs cannot be modeled by first-order logic?

Jose Brox —Preceding unsigned comment added by 83.59.92.128 (talk) 23:24, 20 April 2009 (UTC)

Directed graphs themselves can be expressed in first-order logic. What cannot be expressed in just the language of graphs is the predicate that tells whether two elements of a graph are joined by a path. This can be expressed in first-order set theory but not directly in the language of graphs. The issue is the first order logic is very sensitive to the language used. I agree that language in the article could be more clear. — Carl (CBM · talk) 02:45, 21 April 2009 (UTC)

To add to what Carl says, there are, of course, first-order theories that can express these relationships, and some of them are fairly widely used languages for reasoning about the structure of the WWW. However these languages do not only use first-order concepts of graph theory: typically they are multi-sorted and allow quantification over paths, contain a fully-fledged calculus of relations, or even, as Carl suggests, simply throw in ZFC. It is not reasonable to include such things among the first-order languages of graphs, even though they can be captured in first-order theories. — Charles Stewart (talk) 09:40, 21 April 2009 (UTC)

Thanks for your answers!

Which is then the "simpler" first-order theory that allows talking about paths? And the simpler one for defyning multi(di)graphs? (I can't find a good reference to learn about the model theory of multidigraphs! I want to allow infinite numbers of edges between vertices). Jose Brox —Preceding unsigned comment added by 88.0.98.172 (talk) 14:45, 4 May 2009 (UTC)

"FOL" acronym is worthwhile because?

The current article often deploys the acronym FOL, instead of just printing "First Order Logic". That kind of shorthand doesn't seem useful in a general encyclopedia. Most Wikipedia articles manage to avoid such acronyms, for example the United States article doesn't substitute "USA" every few paragraphs. --AC (talk) 07:47, 22 April 2009 (UTC)

Sounds great to me. Make the edits.--Heyitspeter (talk) 00:55, 6 June 2009 (UTC)

How Can I help?

As a mathematics undergraduate, I am very interested in understanding first-order logic in all its rigor. This article has been repeatedly described as in dire need of revision, so I ask: what are the mistakes in it? How can I help? Would it be better to wipe and restart it? I could put up a sample of a new page somewhere as I continue to learn the subject. Showdownkiller (talk) 15:21, 1 June 2009 (UTC)

If you are still learning about first-order logic it's unlikely that you can help much. The problem is that there are many subtly different ways of presenting it, and that it means different things to different people. What we really need is someone with a good overview over (almost) all presentations of the topic, and with a good grasp of both the mathematical and the philosophical side, to rewrite it. Carl (CBM) is such an editor, and he has already promised to do this. I believe the best way to help him is to be present when he starts, make constructive suggestions but not insist on a particular presentation, and support Carl when someone comes along and insists that the article absolutely must use the peculiar idiosyncratic notation of a book that first appeared in 1960, because "everybody" uses this book. Or, just as likely, when two editors come along with incompatible categorical demands about the article.

I simply don't know if the article contains actual mistakes because I can't force myself to read this heterogeneous mess. It jumps around between different notations, different terminology and different points of view. E.g. philosophers and possibly also some mathematicians seem to love the term "well-formed formulas". To me as a model theorist this sounds about as old-fashioned as "omnibus" and "motorcar"; if you work with these things every day and there is no need for a word for "non-well-formed formulas" (since everybody just calls them strings), then obviously they become just "formulas" (or "formulae"; another potentially contentious issue). Which is exactly what they are in every recent model theory introduction.

I once participated in cleaning up most of the section First-order logic#Syntax of first-order logic. If you read it you will see one of the issues, which was previously not described at all. IIRC, the article simply described the traditional approach but mentioned signatures elsewhere without definitions. (And of course it jumped around between various terms for signatures, such as [first-order] language and vocabulary.)

Another question is "What is a logic?" Some people have started a branch of logic called abstract logic in which they want to compare different logics. They are writing papers that are titled with this question, because there is no consensus what is part of a logic. Is it just syntactical or is the model relation part of it? Is it just semantical or is some notion of derivability part of it? If the latter, does it go as far as a proof theory? This is why this article explains lots of things that are usually discussed in a context of first-order logic, but never actually defines first-order logic itself. --Hans Adler (talk) 20:16, 1 June 2009 (UTC)

Just thought I'd answer the "well-formed formula" (wff) concern you raised, speaking from someone who learned this stuff from philosopher-logicians. The word "formula" does work just as well, and some people do use it (Fitting and Mendelsohn, 1998). The term "wff" is probably better because it makes explicit the fact that there are strings you can write using FOL symbols that don't have any meaning at all (i.e., there are non-well-formed formulas).--Heyitspeter (talk) 00:49, 6 June 2009 (UTC)

I've just got to congratulate Hans for being the first person I've heard describe the natural approach to producing quality articles on specialist topics at Wikipedia. Team work is great, but wide knowledge of sources is also great. Any "knower of sources" can do with plenty of help, especially copyediting, format, general feedback of all kinds. Given that people do pop up insisting on idiosyncracies and we don't want to offend them, or leave "knowers of sources" to deal with such struggles alone, others of us can provide some friendly sourcing of alternatives to the idiosyncratic views and so on.

Regarding wff v formula, I'd have no personal opinion: wff makes explicit what is taken by writers I'm familiar with as assumed. In a journal article, perhaps either term would work fine. In a textbook, I can see reasons either might be considered more user friendly. Here at Wiki, it fits in the textbook side more, I would think (general readership). But frankly, were people to change all wff's to simply say formula, and then do the reverse, I'd not be interested in interfering.

If revisions of the article alternated, differing only by this one exchange, I'd think we had two well formed, synonymous articles, without it mattering which one was visible at any one time. ;) Alastair Haines (talk) 01:54, 6 June 2009 (UTC)

PS I just noticed Hans had tagged a section I'd tried to clean up earlier. I'm just guessing, but I think Hans might prefer use of the passive voice through the article.

1. It can be seen that first order logic is more powerful and descriptive than propositional logic. [passive]
2. We can see that FOL is more powerful. [conversational, non-technical, formal, Stanford Encyclopedia of Philosophy style]
3. You might find FOL more interesting because of its extra power, but we at Wiki think you should remember that comes with costs. [editorial]

(3) is unencyclopedic, but either (1) or (2) is fine, it all depends on: who originally wrote the article, who does most of the re-writing and who does a final copy-edit. If Carl's going to rework things, he should probably write however he feels most comfortable writing, and a final copyeditor could rework style without changing content if there was consensus to use a different tone to Carl's prefered style.

Anyway, best wishes. The article really does need streamlining and it's perfect to have both philosophers and mathematicians working on it. Cheers. Alastair Haines (talk) 06:22, 6 June 2009 (UTC)

OT: What is logic?

If anybody in interested in pursuing that issue (not in this article, of course) there's a volume edited by Dov M. Gabbay called "What is a logical system?". The first essay there by Ian Hacking is "what is logic?" Pcap ping 12:01, 18 September 2009 (UTC)

Which quantifier is more primitive?

It's pretty standard to consider <exists> and <all> as equally primitive. However, it is also well-known that either can be introduced in terms of the other:

• <exists> P(x) iff <not> <all> <not> P(x)
• <all> P(x) iff <not> <exists> <not> P(x)

Peter's recent edit is good to show me that our intuitions vary. My intuition tells me existence is more primitive: it's concrete, I exist, so do many things. To my intuition "everything" is an abstraction: I can't see everything, I don't know everything.

However, I like Peter's intuition. FOL is not there to deal with mere existence, or we'd not have variables, we'd be content with constants: Scotland, Queen Elizabeth II, the Sun, Chelsea FC, Alice in Wonderland, ...

What does the Stanford Encyclopedia of Philosophy say motivated the development of FOL? Does it cover this question? Can we think of search terms to plug into Google (Scholar or otherwise) to find a reliable source on this question?

Keep hacking into this article, Peter. I like your mind. It's a monster of a thing to work it over, but we need a brain like yours wielding the machete. I love logic, and this article can be a love letter. If we get it right, lots of people will be able to understand why we find her beautiful.

Best.

PS You're not related to User:OhNoitsJamie are you, Peter? Alastair Haines (talk) 06:39, 7 June 2009 (UTC)

In the preface to his Begriffsschrift, Frege says that the purpose of his calculus is to expose the logical consequences of propositions, which are not exposed in natural language, and to provide a criterion for the validity of proofs. This motivation is closely related to his logicism. — Charles Stewart (talk) 10:11, 7 June 2009 (UTC)

aka he thought FOL was better than propositional logic... We can include that historical context somewhere in the article if you like but it seems pretty self-evident to me. And p.s. Alastair I agree that the idea of talking about 'everything' seems pretty silly/unweildly/idealistic but it isn't problematic in practice. The universal quantifier usually only restricts conditional sentences. e.g., For all x, if x is an unmarried man then x is a bachelor. Although x technically stands for everything that exists, the proposition only really concerns unmarried men. This is sometimes called "restricting quantifiers".

For example let's say I look in the fridge and say "All the milk has spoiled." Of course I don't mean to be talking about everything in the universe. I'm implicitly restricting quantifiers. We should translate my sentence as: For all x, if x is in Peter's fridge and x is milk, then x has spoiled. Technically, x represents every thing that exists, but all the proposition really concerns is the stuff in my fridge. We really are discussing 'everything' here, but in such a way that we don't run into big philosophical obstacles. Hope that helps. --Heyitspeter (talk) 10:59, 7 June 2009 (UTC)

Oh and even the 'x' in existential quantification (i.e., "For some x") stands for everything that exists. When I say "Something is a person" FOL translates with "For some x, x is a person", which really means "Out of the domain of everything, at least one of those things is a person." We're still discussing everything in the universe when we use existential quantification. So "Which quantifier is more primitive?"? Well as you said, they can be defined in terms of each other so of course they are both equally primitive, but more importantly both run up against the philosophical difficulties that bother you, and in just the same way.--Heyitspeter (talk) 11:04, 7 June 2009 (UTC)

It is relatively common in logic texts that want to just use one quantifier to use only the universal. However, in constructive mathematics where the quantifiers are not interdefinable, the existential quantifier is the more important one. In such contexts, Skolemization is often employed to remove universal quantifiers.

As a side note, remember that the quantifiers do not range over "everything that exists"; in any particular structure there is a set over which the quantifiers range. — Carl (CBM · talk) 11:53, 7 June 2009 (UTC)

Yeah that's especially important in modal contexts where quantifiers range over the domains of specific possible worlds..--Heyitspeter (talk) 01:16, 8 June 2009 (UTC)

PS: I think most of this thread is about predicate logic in general, not first-order logic specifically. Frege would not have recognized what we now call first-order logic.

The division of predicate logic into first-order and higher-order logic came very late in the development of mathematical logic. Frege's original logic was, from a modern point of view, second-order. The Lowenheim-Skolem theorem was stated and proved before the term "first-order logic" was in use. Henkin's construction of first-order models of typed languages, which finally clarified exactly how second-order semantics differ from first-order semantics, was published in 1950. One interesting paper on the development of first-order logic is "The Road to Modern Logic-An Interpretation" by Jose Ferreiros [1] — Carl (CBM · talk) 12:07, 7 June 2009 (UTC)

He he, Carl, comes the hour, comes the man. Yes, I almost wrote my comment to account for non interdefinable quantifiers. I'm currently battling through Nick Asher's Logics of conversation, where skolemization is used, just as you describe. Perhaps that reinforces my feelings regarding existential quantification.

Thanks for the link to Ferreiros article. Is the full text available at PhilPapers? Alastair Haines (talk) 13:21, 7 June 2009 (UTC)

(In response to CBM 11:53, 7 June 2009 (UTC))
Hmm care to explain how the quantifiers can fail to be interdefinable? --Heyitspeter (talk) 01:16, 8 June 2009 (UTC)

The proposition that $\lnot \forall x\lnot \phi (x)$ implies $\exists x\phi (x)$ (with certain restrictions) is called Markov's principle. In the BHK interpretation of intuitionistic logic, $\lnot \forall x\lnot \phi (x)$ is strictly weaker than $\exists x\phi (x)$. A proof of the latter must explicitly demonstrate an example of an x satisfying φ, while a proof of the former need only show that there no uniform effective way of showing, for any given x, that φ(x) entails a contradiction.

I believe there are more general results that show that there is no way, in general, to define either of the quantifiers in terms of the other one. I do not have them at my fingertips, however. — Carl (CBM · talk) 04:05, 8 June 2009 (UTC)

Cool, thanks. If you do find those general results I'd love to hear them. I was thinking about it a bit; you would need to stipulate that all domains are non-empty for $\lnot \forall x\lnot \phi (x)$ to be equivalent to $\exists x\phi (x)$ (even without bringing in intuitionistic logic). We might want to allow empty domains from a philosophical perspective. Do you know of any specifically technical problems doing so?--Heyitspeter (talk) 07:26, 8 June 2009 (UTC)

You've just pointed out another gap in the article. There are several technical issues with allowing empty domains: many of the inference rules that people know for first-order logic are only sound for non-empty domains, e.g. $\phi \lor \exists x\psi \vdash \exists x(\phi \lor \psi )$ when x is not free in φ. Our short article on the subject is at free logic. — Carl (CBM · talk) 13:20, 8 June 2009 (UTC)

Yes, many well-known inference rules fail in empty domains. However, Heyitspeter's equivalence $\exists x\,\phi (x)\leftrightarrow \neg \forall x\,\neg \phi (x)$ is not one of them, it holds in empty models just fine. — Emil J. 13:47, 8 June 2009 (UTC)

Ahh yeah sorry, it was around 4am my time and I was losing it. So I suppose they're equivalent in an empty domain because 1) there is no x-variant of the valuation function v in our model M that satisfies the left side, and 2) it is true that for every x-variant of v in M not-phi(x) is satisfied, since there are no such x-variants, so the right side isn't satisfied either.--Heyitspeter (talk) 17:59, 8 June 2009 (UTC)

Major revisions 2009-6-7

I spent a while today doing some major reorganizational work on the article. As I see it, one main difficulty was that the article had was that the text often repeated itself, as if material was added over time without care to see if it was already present. So I rearranged everything.

I realize this cut the examples that were recently edited in the introduction section; I'm sorry about that. If there is a good way to incorporate them while keeping the flow of the article, that would be great. I think the introduction section I obtained after merging and rewriting flows pretty well, builds the main concepts, and does not assume the reader is already familiar with propositional logic.

The second major problem was with emphasis and gaps in presentation. The compactness theorem was only mentioned as a parenthetical aside. Tableaux proofs were not mentioned at all, and resolution was only mentioned in the section on theorem proving. My viewpoint is that a reference article on first-order logic in general should highlight the main deductive systems; we can put their gory details into subarticles. The sections on inference rules and identities ought to have some additional exposition compared to what I have included.

I removed two of the "limitations" that I thought were either overstated or repeated elsewhere in the article: many-sorted logic and if/then/else.

I hope other people will fix my bad writing, point out any errors I have made, and add the links I have forgotten. — Carl (CBM · talk) 17:14, 7 June 2009 (UTC)

Awesome. Thanks for putting in the work!--Heyitspeter (talk) 18:44, 7 June 2009 (UTC)

There's still a lot to do to make the article complete (even if some things have to be done in a very cursory way). — Carl (CBM · talk) 20:46, 7 June 2009 (UTC)

Of course. It'll happen :) --Heyitspeter (talk) 01:10, 8 June 2009 (UTC)

Outstanding. The article has a more, dare I say it, "logical" flow. :)

Yes, there comes a time when pruning is needed. This pruning looks nicely judicious.

Thanks for so much time. Alastair Haines (talk) 10:53, 8 June 2009 (UTC)

Thanks Carl, good work. Paul August ☎ 15:41, 8 June 2009 (UTC)

Omitted topics?

Thanks to everyone who has been tweaking the writing since the major revisions last week. Are there any remaining significant topics that ought to be covered in the article but are not? — Carl (CBM · talk) 17:43, 15 June 2009 (UTC)

A really significant topic that is missing completely is ${\mathcal {L}}_{\omega }^{\infty }$. That's important because some consider this to be first-order logic. I think it's currently not defined anywhere in Wikipedia, which is a serious omission. Maybe it has to do with the fact that there is no canonical name for this logic.

What I would also like to add is a discussion of what first-order logic is as a mathematical object. Lindström's theorem doesn't make much sense without an answer to this question and the more general one of what is a logic. I am not at all happy with our article Formal system. Recently there have been attempts to give a modular definition of logics that are compatible both with a purely model theoretic and a purely proof theoretic approach. There are also approaches based on institutional model theory. All of this is not very notable, but I think it's needed for a complete treatment of the subject. Hans Adler 11:46, 20 June 2009 (UTC)

Do you mean one of the systems defined at infinitary logic? The definition there is pretty much inscrutable. We could very naturally add a subsection to section 7 about infinitary logic.

I phrased the part on Lindström's in a strange way for exactly the reason you are bringing up: there isn't a general definition of "a logic" to appeal to. I'm not convinced that this article is the place to cover that, but if it were covered somewhere else we could find a way to allude to it. — Carl (CBM · talk) 12:09, 20 June 2009 (UTC)

Truth in empty domains

I'm lost in the section on empty domains where it reads: "The definition of truth in an interpretation that uses a variable assignment function cannot work with empty domains, because there are no variable assignment functions whose range is empty." (p.s., this reminds me that we need a section on what an interpretation is.)

Of course the range is empty if the domain is, but more importantly, I don't understand how this is a problem for truth. An interpretation can make reference to nonexistent variable assignment functions. For example $\forall x\phi (x)$ is true iff for every variable assignment the assigned terms satisfy phi. If there is no variable assignment then it comes out true. I'm probably confused, and this particular terminology is unfamiliar to me, but I thought I'd ask anyways. --Heyitspeter (talk) 08:58, 17 June 2009 (UTC)

The definition given higher up says one must start with a variable assignment function before any truth values can defined, even for atomic formulas. In the variable assignment approach, for example as presented by Enderton, every formula is given a truth value, even ones with free variables. This cannot get off the ground if there is no variable assignment function at all. This technicality is why the definition has to be changed to handle empty domain.

You are right that the ad hoc way of dealing with quantifiers is to declare all universal statements true and all existential statements false. This is exactly what I mean by treating an empty domain as a special case. — Carl (CBM · talk) 12:15, 17 June 2009 (UTC)

(edit conflict) The problem is that in the standard definition one does not directly define the truth value of a sentence. Rather, one defines inductively the truth value of a formula under a given assignment, and then the truth value of a sentence is its value under some, or equivalently, any, assignment. Since there are no assignments in an empty domain, this definition breaks down there: depending on which of the two versions of the definition is used (they are no longer equivalent), it would either make all sentences false, or it would make all sentences true. In order to obtain the intuitively expected behaviour that $\forall x\,\phi (x)$ is true and $\exists x\,\phi (x)$ is false in an empty domain, the definition has to be modified, for example we can reformulate it so that it works with partial assignments, defined only for variables which actually occur free in the formula. — Emil J. 12:22, 17 June 2009 (UTC)

So basically we have the choice between presenting the standard way of doing things, plus a kludge to accommodate empty domains as an arbitrary special case; or coming up with clean definitions. Obviously the right thing to do from a mathematical point of view is to assign truth values only to those variables that occur freely in a formula. The latter approach is slightly more complicated because we need different types of assignments for different formulas. I am not aware of any text that is doing it this way, but it should exist somewhere. I would be surprised if people in categorical logic wouldn't do it that way, for example.

This is just one example for the general problem that there are many little and not so little details in which various versions of first-order logic differ:

• empty domain allowed or not
• infix or polish notation for logical connectives
• standard or polish notation for functions and relations
• exact choice of logical connectives and quantifiers, perhaps most importantly:
  • whether there is a nullary connective
• fixed signature or varying signatures
• nullary predicates (propositions) allowed or not
• with or without equality
• formulas are strings or trees
• infinite conjunctions/disjunctions are allowed or not
• similar issues related to deductions.

There seems to be no silver bullet for this problem. If we discuss everything in place (such as the signature problem in the current version) it gets incredibly confusing. If we go with tradition in each case, it's going to be quite problematic as a basis for our more advanced articles. But making the mathematically best choices is not only impossible in some cases (i.e. strings are better if we want to feed formulas into Turing machines, trees are beet if we want to do model theory of ${\mathcal {L}}_{\omega }^{\infty }$) but would be a disservice for the majority of our readers.

I wonder if we can approach this problem by giving two complete definitions of first-order logic: A "conservative" one and a "progressive" one that basically makes the opposite choices as far as sensible and practicable. I am not sure whether they should be on the same page or on different pages, and whether both of them even need to be contiguous. One could be spread over a series of articles such as Syntax of first-order logic, Semantics of first-order logic, Deduction in first-order logic(?) that could be used from here per WP:Summary style. Or the "progressive" definition could be in a new article Extensions of first-order logic. Hans Adler 12:35, 20 June 2009 (UTC)

To be fair, the standard way of doing things doesn't permit empty domains. So I would say the right thing, from a mathematical point of view, is not to allow the domain to be empty... This is why it seems fine to me to just say "here is how to kludge around them if you want to".

I do think that the articles on particular deductive systems should be more clear about the details of those systems. But I don't think it's necessary for us to completely document several different formal definitions of first-order logic. I think our article should simply summarize the real world, and let people use actual texts if they want completely detailed formal presentations.

As to formulas being trees, or allowing infinite disjunctions, these are really only seen in model theory. For the vast majority of authors, formulas are simply finite strings. We should definitely mention the more abstract viewpoint, but we don't need to write the article around it. — Carl (CBM · talk) 13:00, 20 June 2009 (UTC)

Yes, I am not trying to push these things into this article; but they should be done somewhere, so that they can essentially be ignored here to simplify things, and so that we can link to them from more technical articles that need them. Perhaps a new article Extensions of first-order logic is the right context for introducing FO logic with empty domains, formulas as trees, infinite conjunctions/disjunctions and quantification over infinitely many variables.

By the mathematical POV I mean taking into account the connections to other fields. E.g. there should be no doubt at all that posets may be empty; otherwise the ordinal 0 wouldn't be a poset. Wouldn't it be strange if we could describe the category of posets as an elementary class, except that exactly one object doesn't exist for us? It's a bit like defining the natural numbers so that they don't include 0. It's traditional, but not optimal. Hans Adler 13:31, 20 June 2009 (UTC)

Thanks for starting a section on infinitary logic. That article wasn't on my watchlist, and I wasn't aware of it. Perhaps I should hijack this article for my plan? Let me know when you are finished so I can do a few necessary corrections. Hans Adler 13:46, 20 June 2009 (UTC)

I agree that we should cover the variations somewhere: in this article. Please do feel free to improve the section on infinitary logic; I just threw something down to start the process. We can mention empty posets in the section on the empty domain, which needs a good example anyway. But I have never seen a good outcome when articles are split up because of distinctions between fields; look at the mess with the articles(!) on propositional logic, and the articles(!) on decidability.

The infinitary logic article would be a good place to explain in detail how to represent formulas as trees (if this is necessary; it seems so obvious). That whole article is in need of improvement. Of course that article should be a separate article from this one; don't misread my argument above.

At a higher level, I think it is important to emphasize the unity of first-order logic. Of course there are variations, and we should discuss them, but there is a reason that computer scientists, philosophers, and mathematicians all call their system "first-order logic". The phenomenon that any two systems that occur in practice and be translated into each other in an obvious way gives strength to the argument that first-order logic is a system of foundational importance. This sort of robustness to minor change occurs in a few other places, most notably Turing computability. We would do a disservice to our readers if we left them with the picture that first-order logic is a fragmented collection of different systems (as intuitionistic logic might be regarded) rather than a single concept which different fields have adapted to their purposes. — Carl (CBM · talk) 13:57, 20 June 2009 (UTC)

quantification theory

Could someone explain why it redirects here. I removed a statement about the term, but I reverted myself, as I'm not sure it isn't correct. — Arthur Rubin (talk) 01:59, 19 November 2009 (UTC)

It's a less common term for first-order logic but I have seen it before. — Carl (CBM · talk) 03:47, 19 November 2009 (UTC)

Could it not be confused with the study of more general types of quantifiers beyond for all and there exist. Such as there are aleph-1 or more of whatever. Or infinite conjunctions. See infinitary logic. Or Henkin quantifiers. JRSpriggs (talk) 04:00, 19 November 2009 (UTC)

I agree that the term sounds more broad than just first-order logic. But Mendelson's Introduction to mathematical logic, for example, uses "quantification theory" as the title of the chapter on first-order logic. — Carl (CBM · talk) 04:28, 19 November 2009 (UTC)

This justifies the redirect, but not this prominent mention in the article. The claim that quantification theory is the "theoretical study of first-order logic" also seems to be misleading to me; if it makes any sense at all then surely only in a philosophy context? Hans Adler 09:09, 19 November 2009 (UTC)

The sentence was worded a little strongly, so I just merged the term into the list of synonyms. — Carl (CBM · talk) 12:10, 19 November 2009 (UTC)

sentence doesn't belong to introduction IMO

I think the following sentence should be removed from the introduction paragraph.

"A history of first-order logic and an account of its emergence over other formal logics is provided by Ferreirós (2001)."

There's nothing wrong with it wrt its /content/, but it's a statement about the article rather than about FOL, I would say, and the introduction should be kept as concise and relevant as possible.

I'm putting it up for discussion here, but unless someone strongly object, I would like to delete it (and fit the sentence into another section, later in the article).

-- Minvogt (talk) 13:54, 13 January 2010 (UTC)

It is usual for articles to have history sections. This article does not. The sentence you mentioned is the last sentence in the lead and may be regarded as a substitute for having a history section. There is no better place for it in this article. So leave it where it is. JRSpriggs (talk) 10:39, 15 January 2010 (UTC)

What about moving it to the "references" or "further reading" section? along with a label?--Heyitspeter (talk) 20:42, 16 January 2010 (UTC)

The reference is already there — "*Ferreirós, José (2001), "The Road to Modern Logic-An Interpretation", Bulletin of Symbolic Logic, 7 (4): 441–484, doi:10.2307/2687794.". The sentence just informs the reader that it is there. JRSpriggs (talk) 00:33, 17 January 2010 (UTC)

I don't think there is a much of another section where the sentence would fit. Really, the article could use a history section. But I don't like the idea of not mentioning the Ferrerios reference in the article at all. It's a high-quality reference, and readers looking at an encyclopedia article may well want to know about the history of the topic, so pointing out that reference seems like a good thing for the article to do. — Carl (CBM · talk) 03:19, 18 January 2010 (UTC)

I see your point. I still think it's looks sort of clumsy, but I guess 'form follows function' applies here. -- Minvogt (talk) 02:01, 2 March 2010 (UTC)

I think this was explained above. The article could still use a history section IMHO but the reference is at least a start. — Carl (CBM · talk) 01:31, 21 May 2012 (UTC)

This sentence is somehow unusual but acceptable, provided that Ferreirós 2001 is really a/the fundamental book on the matter. --Nemo 15:34, 31 March 2017 (UTC)

Mistake in definition of free variable?

Third point in the definition says "Binary connectives. x is free in (φ --> ψ) if and only if x is free in either φ or ψ. x is bound in (φ --> ψ) if and only if x is bound in either φ or ψ. The same rule applies to any other binary connective in place of -->." But this seems contradictory. If x is free in φ and bound in ψ, both conditions are satisfied. Surely x must be bound in φ and ψ to be bound in (φ --> ψ). Kronocide (talk) 16:33, 30 December 2010 (UTC)

A variable can have both free and bound occurrences in the same formula; like "open" and "closed" in topology these are not exclusive. However, in practice people usually avoid formulas such as $(\exists x)(P(x,y)\land (\forall y)Q(x,y))$ by renaming one of the ys to something else. In that formula, y has both a free occurrence and a bound occurrence. The definition in the article here is identical to the one in Hinman, Fundamentals of mathematical logic, 2005, p. 100. — Carl (CBM · talk) 17:04, 30 December 2010 (UTC)

I see. I was (erroneously) thinking of the variables rather than their symbols (such that variables would be individuated by distinct scopes in the formula). Thanks for putting me straight. Kronocide (talk) 14:28, 2 January 2011 (UTC)

lede

Is the following in the lede quite correct (emphasis added)?

Briefly, first-order logic is distinguished from higher-order logics in that quantification is allowed only over individual variables (but not, for example, over propositions). Philogo (talk) 23:44, 6 January 2011 (UTC)

I disagree with higher-order logics having quantification over propositions; it really is over sets. Tkuvho's modification is better. — Arthur Rubin (talk) 10:02, 7 January 2011 (UTC)

The article on higher-order logic says:

In mathematics and logic, a higher-order logic is distinguished from first-order logic in a number of ways. One of these is the type of variables appearing in quantifications; in first-order logic, roughly speaking, it is forbidden to quantify over predicates. See second-order logic for systems in which this is permitted. Another way in which higher-order logic differs from first-order logic is in the constructions allowed in the underlying type theory. A higher-order predicate is a predicate that takes one or more other predicates as arguments. In general, a higher-order predicate of order n takes one or more predicates of order n − 1 as arguments, where n > 1. A similar remark holds for higher-order functions.

Is that not correct (no mention of sets)? i.e 1. it is really over neither propositions nor sets but predicate variables over which quantification is allowed 2. It allows higher order predicates , higher-order predicate being a predicate that takes one or more other predicates as arguments. The two articles do not seem to say the same thing and, surely, they should and do so precisely. Philogo (talk) 19:40, 7 January 2011 (UTC)

Other editors keep reverting one another in the lede with no discussion on this talk page. Philogo (talk) 21:54, 8 January 2011 (UTC) My understanding is that the adjective "first-order" is used to distinguish first-order theories from theories in which there are predicates having other predicates or functions as arguments or in which predicate quantifiers or function quantifiers are permitted or both. Mendelson,Elliot: Introduction to Mathematical Logic, Von Nostrand Reinhold 1964, page 56. Is that not correct? I have never heard of quantification over propositions.Philogo (talk) 01:14, 9 January 2011 (UTC)

The above being uncontested I have implemented accordingly. If there is such a thing as quantification over propositions I would be interested in further details Philogo (talk) 14:58, 9 January 2011 (UTC)

Predicates provide an intensional description of relations and in particular functions, i.e., sets. Quantification over predicates can therefore be thought of as quantification over sets. The most naive formulation of ZF therefore involves higher-order quantification. Now one can write it as first-order by using variables for sets, but I think this is a different, "larger", meaning of the expression "first-order". I signaled this problem at WPM and expect further input from editors. This problem is not going to go away without some effort; note that the page second-order logic uses the term in the narrow meaning. Tkuvho (talk) 15:04, 9 January 2011 (UTC)

Thanks for that. Meanwhile I have discovered quite a bit about quantification over propositions dating right back to Russell (e.g. Because propositions are entities, variables for them in Russell’s logic can be bound by quantifiers. in http://www.iep.utm.edu/par-rusm/) As I said I have not heard of such before. Bearing in mind that this article is about first-order logic, and that the lede has been attempting to explain why it is so-called (first-order) to somebody who does not already know, do you think that my edit does the job? If (as appears to be the case) there is such a thing as quantification over propositional quantifiers (as well as predicate quantifiers or function quantifiers) and if such logics are known as higher-order logics then we could incoporate this into the lede for the sake of completeness (although the citation to Mendelson would no loger be accurate.) Philogo (talk) 15:38, 9 January 2011 (UTC)

Well, it would be helpful to include the narrow meaning of "first-order", as on the second order logic page, where quantification is over individuals as opposed to sets. This is certainly a commonly used sense of "first-order". It also happens to be the easiest sense to explain to a novice. When one talks about the first-order theory of the real numbers, one means the theory that excludes, for instance, the least upper bound property, which involves quantification over sets. Tkuvho (talk) 16:00, 9 January 2011 (UTC)

I guess the issue is whether one allows plural quantification. Tkuvho (talk) 16:03, 9 January 2011 (UTC)

I am not sure I have grasped the distinction between narrower and wider meaning you allude to. It seems to me that there are two distinct restrictions on first-order logic reoved w.r.t higher order logics, as stated by Mendelson. 1.The domains of (arguments of) predicates in FOL are resticted to individuals wheras in HOL the domains of (arguments to) predicates include predicates or functions as well. Thus in FOL there are FO predicate symbols whose arguments must be (in wffs) individual constants or (individual) variables. In SOL and HOL domains of (arguments to) predicates include predicates or functions as well, represented by n-order predicate symbols. Note that this extension does not allow quantification over predicates, since it does not extend to predicate variables. It would alow representation of (if you forgive a non-mathematical example) adverbs If John ran quickly then Jon ran. 2. In FOL quantification is allowed over (individual) variables (they are the only sought of variable allowed). SOL and HOL allow quantification over predicates represented by n-order predicate variables and/or over functions represented by function variables. It would alow representation of (if you forgive a non-mathematical example) adverbial variables: If John ran in any manner then John ran. - However he ran he ran. These to me seem distinct extensions to FOL.

Your edit a little while back had first-order logic is distinguished from higher-order logics in that quantification is allowed only over individuals (but not, for example, over sets of individuals). This appears to allow the second extension but not the first. Perhaps I have missed something. You do not appear to be biting the bullet about whether HOL also allows 3. quantifiction over propositions and if so whether it is worth mentioning in this article. I do feel quite stronly however that the articles (on FOL, SOL and HOL) should be compatible.Philogo (talk) 18:50, 9 January 2011 (UTC)

You asked me to clarify my distiction between two types of first-order as I see it. Consider the property that "for every set A of real numbers, if A is bounded then there is a least upper bound for A". What's the order here according to your book? Tkuvho (talk) 19:38, 9 January 2011 (UTC)

Feeling my way, you are talking about two types of fo predicate logic, correct? I do not want to misunderstnad as a result of weekness in my maths, and I suspect I am not sure what a least upper bound would be. The problem is whether you can represent in FOL a statement of the form For every set A (eg real numbers), if set A has a property F (eg bounded) then then there exists a y (eg an upper bound) such that R(A,y) (eg. y is the upper bound of A). Would either of the following homlier examples pose the same problem: 1. For every finite set of numbers one member of that set is the highest? 2. For every finite set of numbers there is am upper range? 3. For every finite set of numbers there is a mean value? 4. For every finite set of massive objects there exist a centre of mass? I am aware of the following problem. When a predicate is applied to a set it may be applied distributively or non-distributively, see Predicate (grammar)#Collective_vs._distributive_predicates In the former case the predicate applies to each member of the set in the latter case to the set per se. Eg The Legion was brave (each member was brave) - distributive application of brave. The Legion was decimated (reduced by one tenth) - non distributive application of decimated - no individual soldiers was reduce by one tenth. If we have a theory in which all predicates are applied non-distributively to sets to then we can consider the domain to consist of these sets, treating each set as an individual (although not without controversy, as discussed in Plural quantification) If we have a theory in which all predicates are applied distributivly then the domain can be treated as consisting of the individuals that consitute the sets. The problem arises if we wish to have predicates some of which apply distributively and other non-distributively. eg If any Legion is not brave(distrib) it will be decimated (non-distib). Now we seem to need a domain of Legions (sets of men) as arguments for the decimation predicate but also a a domain of individual men (as arguments to the brave predicate.) Is this the same problem (mixture of distrib and non-distrib predicates) that your maths example illustrates?Philogo (talk) 21:34, 9 January 2011 (UTC)

Mendelson's description you quote is in line with the common usage of the term "first-order". As you discovered, there are higher-order logics that include quantifications over propositions. They are used, for example, to reason about the logics of computer programs. This does not mean all higher-order logics beyond the first-order ones would include them. (Correcting the name of Elliott Mendelson)Lauri.pirttiaho (talk) 20:25, 9 January 2011 (UTC)

In that case would you be happy if I amend to

The adjective "first-order" is used to distinguish first-order theories from higher order theories in which there are predicates having other predicates or functions as arguments or in which predicate quantifiers or function quantifiers are permitted or both and/or quantification over propositions. Philogo (talk) 21:34, 9 January 2011 (UTC)

Exhaustive listing is probably not needed. The current form is in line with the common usage and there is a link to HOL's page. It would be more useful now to extend that one. — Preceding unsigned comment added by Lauri.pirttiaho (talk • contribs) 15:39, 14 January 2011 (UTC)

The lede misquotes Mendelson as writng:

• The adjective "first-order" is used to distinguish first-order logic from higher-order logics. In such theories, there are predicates having other predicates, sets, or functions as arguments or in which predicate, set, or function quantifiers are permitted.

what he wrote was

• The adjective "first-order" is used to distinguish first-order theories from higher order theories in which there are predicates having other predicates or functions as arguments or in which predicate quantifiers or function quantifiers are permitted or both. Philogo (talk) 16:26, 16 January 2011 (UTC)

Philogo (talk) 16:30, 16 January 2011 (UTC)

Right. Mendelson did not say "set". Actually I was not aware of the fact that the sentence was a direct quotation from Mendelson (before "sets" were added, that is). At any rate, a set defined intensionally using a predicate is, to many mathematicians, an adequate substitute for the predicate, though of course there are criticisms of such philosophical bias, as already discussed. Could we perhaps add something in the footnote to clarify that Mendelson did not say "set"? It would be helpful if someone could provide a source that makes the point I mentioned, if it is correct. Tkuvho (talk) 17:00, 16 January 2011 (UTC)

I don't think you can really quote someone and then add something in a footnote saying that they actually said something different. I would suggest 1. we quote Mendelson correctly, and 2. if felt necessary, adding a second sentence explaining the relationship between predicates and sets. Philogo (talk) 18:22, 16 January 2011 (UTC)

That might be a solution. Alternatively (perhaps better), perhaps there is another logic textbook dealing with this issue. Tkuvho (talk) 18:36, 16 January 2011 (UTC)

In that case, do you agree with my reinstating the quote from Mendelson, which could then be followed by "in other words" to be followed by a second sentence explaining the relationship between predicates and sets, or other such explanatory remarks, possible in the form of a quotation from an alternative text. Nobody seems to want to say that Mendelson is wrong, rather that there is more that should be said. Perhaps the problem is that Mendelson quote is comparing just the syntax of FOL and HOL; what is missing is a comparison of the semantics. Philogo (talk) 18:47, 16 January 2011 (UTC)

OK, that may be better. Would you like to volunteer an extra sentence? Tkuvho (talk) 18:58, 16 January 2011 (UTC)

Done; for some reason extra bit in italics.

I strongly prefer the shorter sentence in the lede, along with a longer description lower in the article. On the one hand, the quote from Mendelson isn't quite complete, because the semantics are a key part of the difference – you absolutely can quantify over predicates in multi-sorted first order logic, as long as you use first order semantics. On the other hnd, the lede is not the place to go into great depth about these things. Most people who learn first-order logic don't learn higher-order logic, and so we don't need to try to summarize it in one sentence in the lede. — Carl (CBM · talk) 20:22, 16 January 2011 (UTC)

I think the Mendelson quote is incomplete because,as I suggested above, the problem is that Mendelson quote is comparing just the syntax of FOL and HOL; what is missing is a comparison of the semantics. I think Tkuvho does not like the shortened version becuase sets do not get a look in. No doubt some would want to see mention of properties and properties of properties. Editors (inc. me) tend to get over-anxious about what is in the lede, when there is the rest of the article to go into the nicities (sp?). I think the lede would be good enough if it suggested why first-order logic is so called. The Mendelson quote is from just a footnote intended to satisy such curiosity without going into detail. He added, BTW, "First-order theries suffice for the expression of known mathematical theories and, in any case, most higher-order theories can be suitable "translated" into first-order theories." If true, it is surely TMI for the lede; if not true then the new section "Expressivenes" would be the place to discuss that. Is it true I wonder? Philogo (talk) 20:44, 16 January 2011 (UTC)

cf Interpretation (logic)#Higher-order predicate logicsPhilogo (talk) 22:32, 16 January 2011 (UTC)

plural quantification

I am starting a new thread because the previous one is getting unmanageable. Yes, collective versus distributive is the issue. The grammar page you referred me to is understandably not sensitive to the problem of infinite sets. At plural quantification there is obviously more awareness of it. Now this page cannot be solely a page about grammar, as first order logic is commonly used in math as you might imagine. Numerous mathematicians think of quantification over sets of individuals as second-order quantification. This is what was causing the misunderstandings over the lede during the past few months. I think the mathematicians' viewpoint should be reflected here as well. Tkuvho (talk) :32, 10 January 2011 (UTC)

Sorry to refer you to a grammar page: to my suprise there was no wiki logic/philosophy articles on distributive and non-distributive predication. The following gives a better account: http://plato.stanford.edu/entries/plural-quant/index.html It seems to me that (a) if you have only distrib preds then you can use FOL preds in the normal way (b) if you have only non-distrib preds you can represent then by second order preds or you could allow plural quantification in FOL. (c) if you have both distrib preds and non-distrib preds (as in the examples discussed above and, I think, in the famous Some critics only admire on another then you would have to either us SOL with SO predicates and FO predicates or do some fancy footwork with plural quantification. The situation represents a dilemma for philosophy (of logic). (a) If we allow SOL (and higher) without the caveat that it is a mere convenience and can be reduced to FOL then we pay the price of ontological commitment to the existence of predictates, sets and propositions in addition to objects. The fear of Realism and what it entails is over two thousand years old. (b) If we do not allow SOL (and higher) then we seem unable to handle very simple problems, e.g. the logic of adjectives and adverbs. Surely "all green men are men" and "all who are running quickly are running" are logical truths but tricky to cast into FOL, as is "Roses are red and red is a colour". My impression is that mathematicians are not too bothered by Realism. I do not know whether there are mathematical equivalents of the adjectives and adverbs problem described, but essentially the same problem arises with any predicates applicable non-distributively, an eg being (if I understnad it) yours regarding the boundaries of bounded sets. Philogo (talk) 02:25, 10 January 2011 (UTC)

What do you see as the problem with Realism in your comment on item (a)? Tkuvho (talk) 06:20, 10 January 2011 (UTC)

Oh dear: I have two "a"s above. I do not think item (a1) creates any problems. (you have only distrib preds and use FOL preds in the normal way) Ontological commitment is restricted to the elements of the domain. (If the domain includes abstract objects, the problem is not created by the use of FOL.) With (a2) (use SOL and higher (without the caveat that it is a mere convenience and can be reduced to FOL) we pay the price of ontological commitment to the existence of predictates, sets and propositions in addition to objects In other words we are ontologically committed to entities in addition to the objects (initially) cited as elements of the domain, i.e a "torrent of universals".

"By treating predicate letters as variables of quantification we precipitated a torrent of universals against which intuition is powerless" - Quine, Reification of Universals, para 6, in From a logical point of view, Harper, 1953/1961.Philogo (talk) 21:30, 10 January 2011 (UTC)

Right, that's what I thought you would say. I hasten to mention that I am sympathetic to Quine's criticism. The ontological assumptions made in current mathematical practice could be questioned from a philosophical perspective. However, it is not the purpose of an encyclopedia to be prescriptive. The current mathematical practice being what it is, the "torrent of universals" is ironically a day-to-day reality one can't ignore. Mathematicians do assume the existence of sets. That's what ZFC is all about. Editing this page so as to fight such a reality is not really what we should be doing. Tkuvho (talk) 06:05, 11 January 2011 (UTC)

I have no argument with that. Philogo (talk) 20:22, 11 January 2011 (UTC)

The syntax of any effective (humanly usable) system of logic can be mapped into a model in FOL+ZFC by some suitable encoding of types as elements of certain sets. Thus all logics strong enough to model FOL+ZFC are effectively inter-convertable at the level of syntax. Thus if second order logic is to be substantially different, it can only be so semantically. That is, it must include some non-effective notion such as: a "standard model" of arithmetic only has the "actual" natural numbers, i.e. mathematical induction works even for indescribable predicates; a "maximal-width standard model" of set theory is V_α together with the restriction to it of the actual element relation. JRSpriggs (talk) 09:23, 10 January 2011 (UTC)

Hi JR, Thanks for your contribution. What would you recommend as far as the lede is concerned? Tkuvho (talk) 10:43, 10 January 2011 (UTC)

Restrictions, extensions and variations

The paragraph Restrictions, extensions and variations does not mention polish notation under Restricted languages. Philogo (talk) 20:41, 11 January 2011 (UTC)

Of course not, it isn't a restriction, just a different way of writing the same thing. The article does mention Polish notation in the 'Notational conventions' section, which is appropriate. — Carl (CBM · talk) 20:53, 11 January 2011 (UTC)

Mot sure about "of course". Some of the other "restictions" mentioned in the paragraph are also surely equaly "ways of writing the same thing." Perhaps they should be under variations.Philogo (talk) 21:10, 11 January 2011 (UTC)

Polish notation has all the same quantifiers, connectives, and types of symbols that the usual syntax has. It is written in a different order, and has a different convention for parentheses. The restrictions listed in the restrictions section actually restrict things (e.g. no existential quantifiers, no binary functions) which are not restricted in Polish notation. — Carl (CBM · talk) 21:17, 11 January 2011 (UTC)

Precisely; and "different convention for parentheses" would be a 'variation', would it not?Philogo (talk) 22:55, 11 January 2011 (UTC)

It seems to me that the "notational conventions" section, where Polish notation is already mentioned, is a fine place for it. I don't see why it needs to be mentioned a second time just because some section title has the word "variations"? Really that word could be removed, I think that "restrictions and extensions" would match the content there. — Carl (CBM · talk) 23:04, 11 January 2011 (UTC)

It make sense that the lable sense what is in the tin. Philogo (talk) 23:08, 11 January 2011 (UTC)

quantifications over propositions

Lauri.pirttiaho has pointed out that there are higher-order logics that include quantifications over propositions. They are used, for example, to reason about the logics of computer programs. This does not mean all higher-order logics beyond the first-order ones would include them. He had origially suggested that this should be in the lede as the characteristic of higher-order logic distinguishing same from FOL. As it is quantifications over propositions is not mentioned in the article as a characersitic of any HOL. The issue having been raised, it would be better resolved. Philogo (talk) 23:23, 11 January 2011 (UTC)

The article lede says right now,

"The adjective "first-order" is used to distinguish first-order theories from higher order theories in which there are predicates having other predicates or functions as arguments or in which predicate quantifiers or function quantifiers are permitted or both."

It's mostly a matter of taste whether you replace the word "predicate" with "proposition", or "set" there. It seems common to me for more philosophical authors to use a "predicate" based setup and more mathematical authors to use a "set" based setup. I wouldn't be surprised if someone else uses "propositions", although I think "predicates" is much more common if that's the intended meaning. The philosophical difference between an arbitrary set and an arbitrary predicate is not a key point. And, as JRSpriggs said above, the real difference is in the semantics, not the syntax. — Carl (CBM · talk) 23:38, 11 January 2011 (UTC)

I can't say I agree that "It's mostly a matter of taste whether you replace the word "predicate" with "proposition": I do not see them as at all equivalent, and I have never heard them used synonymously. There are many of us who are at least a little uncomfortable with the term and concept of "proposition": I think you can blame Quine for that. (The terms proposition symbols or propositional variable are OK although sentential symbol or sentential letter)

The current bit of the lede you quote is result of my edit, to resolve a bit of a revert war, anf is a quote from Mendelson (who as I recall is not admired by your professor).

Until Lauri.pirttiaho mentioned it I had never heard of "quantifications over propositions". A little investigation reveals a literature going back to the time of Russell, and my impression is that "quantifications over propositions" is something quite different to "quantification over predicates".

BTW I agree that "It is common to for more philosophical authors to use a "predicate" based setup and more mathematical authors to use a "set" based setup." I am not sure how or when this came about. It would be great if the article were written that was of equal comfort to both. In the texts with which I familiar (a) predicates and predicate letters (or symbols) are synoynmous; there is not distiction correspondng to that between number and numeral. (b) Predicate letters are said to of n degree and a n-ary predicate letter followed by a string of n individual symbols is an atomic formula. (c) An interpretation assigns to each n-ary predicate letter an n-place relation in the domain. Thus a predicate (i.e a predicate symbol) is not a set; it is assigned to set by an interpretation. Perhaps the lede might say

• The adjective "first-order" is used to distinguish first-order theories from higher order theories. In first-order theories (a) predicates may have only individuals as arguments, and are assigned by an interpretation to sets of individuals (b) quantification is allowed only over individuals. Higher order theories may allow (a) predicates having other predicates or functions as arguments, and are assigned by an interpretation to sets of sets, (b) predicate quantifiers or function quantifiers are permitted.

Philogo (talk) 01:19, 12 January 2011 (UTC)

(1) I don't think that the lede needs to be particularly detailed, and really there isn't room there.

(2) The difference is not syntactic. It makes no difference what types of arguments things can have. Indeed, my main area of research is second-order arithmetic, which is a first-order(!) theory in which we can quantify over numbers, sets of numbers, predicates of natural numbers, and many more such things. So if the goal were really to explain the difference, we can't do it by saying something about being able to quantify over sets. The difference of higher-order logic is entirely in the semantics, not in the syntax.

(3) Regardless of (2), I am OK with the current lede, because there really isn't room there to try to go into detail. The article on second-order logic explains it well enough. — Carl (CBM · talk) 01:33, 12 January 2011 (UTC)

If the term "first-order" is used in two significantly different senses, this should be explained somewhere in wiki. Tkuvho (talk) 05:51, 12 January 2011 (UTC)

It's not; "first-order logic" means "first order logic", and second-order logic means second-order logic, although one has to be clear about the intended semantics. So it isn't a problem here, and the article on second-order logic (semantics section) points out that there are two possible semantics there. — Carl (CBM · talk) 12:32, 12 January 2011 (UTC)

Are you saying that the assertiion that "in first-order logic quantification is allowed only over individuals but not sets of individuals" should be described as "Henkin semantics"? Tkuvho (talk) 17:33, 12 January 2011 (UTC)

In first-order logic it is perfectly possible to quantify over sets of individuals. Just add another type of variable for sets, and the set membership relation. This is what is done in second-order arithmetic, which is a theory in first-order logic. In general, you cannot tell just by looking at the syntax, which type of logic is being used.

The distinguishing feature of higher-order logic is that the standard "full" semantics allow the set quantifiers to range over the entire powerset of the set of individuals, while in first-order logic each interpretation may restrict the set quantifiers to some subset of the powerset of the set of individuals. So first-order logic corresponds to Henkin semantics, while second-order logic corresponds to full semantics. But this is way too much information to try to present in the lede of the article on first-order logic. Most introductory books on first-order logic don't even mention higher-order logic. — Carl (CBM · talk) 18:02, 12 January 2011 (UTC)

I understand that this constitutes a consistent way of explaining the qualifier "first-order", but isn't it frequently used in the sense I mentioned? Surely you have come across statements of the sort "first-order theory does not quantify over sets". Elementary theory of the reals is often referred to as first-order theory. I think anyone looking at first-order logic would expect to see some hint of this, as do I and Arthur (see recent edits). Tkuvho (talk) 18:13, 12 January 2011 (UTC)

(1) ZFC is a first-order theory that can quantify over sets, and in a different sense so is second-order arithmetic.

(2) The article does say something about this, in the lede: "The adjective "first-order" is used to distinguish first-order theories from higher order theories in which there are predicates having other predicates or functions as arguments or in which predicate quantifiers or function quantifiers are permitted or both." Like I said, the choice between "predicates" and "sets" is just a matter of taste. I don't see what else the lede could sensibly try to include. — Carl (CBM · talk) 18:18, 12 January 2011 (UTC)

We are talking past each other. I am not talking about the difference between sets and predicates. I understand that ZF can be formulated as a first order theory, but that sense of "first-order" is not the one that is needed, for example, to express the transfer principle in Robinson's theory. Frequently the transfer principle is formulated by saying that R* has the same first-order properties as R. This becomes unintelligible if first-order quantification is taken over sets (unless of course "set" means "internal set"). Tkuvho (talk) 19:40, 12 January 2011 (UTC)

Here is the first sentence of our page elementary equivalence: "In model theory, a field within mathematical logic, two structures M and N of the same signature σ are called elementarily equivalent if they satisfy the same first-order σ-sentences." Here "first-order" is linked to "first-order logic". Is that the same notion of "first-order" as defined in this page? Tkuvho (talk) 11:38, 13 January 2011 (UTC)

Yes. They are already working in first-order logic, and when they say "first-order property" or "first-order sentence" they just mean a property that can be expressed in the language of the theory at hand (that is, in the language of the object theory rather than the metatheory). That language might include variables for sets, as in second-order arithmetic. — Carl (CBM · talk) 13:16, 13 January 2011 (UTC)

Perhaps we could add a sentence at the end of the lede on informal usage, such as "Informally, first-order formulas are frequently understood in the sense that quantification is allowed over individuals but not sets of individuals, see for instance Elementary equivalence." Tkuvho (talk) 12:29, 13 January 2011 (UTC)

That would just duplicate the sentence that is already in the lede. I edited that sentence in the article to add the word "sets". I don't think there is any reason to link to elementary equivalence there, just because that article happens to use the term "first-order property". Especially because a given first-order theory may allow quantification over sets – we have to remember that the description in the lede is just suggestive, but isn't literally true. — Carl (CBM · talk) 13:16, 13 January 2011 (UTC)

Brilliant. Tkuvho (talk) 13:30, 13 January 2011 (UTC)

Is the current version, The adjective "first-order" is used to distinguish first-order theories from higher order theories in which there are predicates having other predicates, sets, or functions as arguments or in which predicate, set, or function quantifiers are permitted meant to imply that (a) a predicate may take either another predicate or a set as an argument or (b) that the terms "predicate" and "set" are synonymous? In the texts with which I familiar predicates and predicate letters (or symbols) are synoynmous, not "predicate" and "set". What is the objection to my earlier suggest: The adjective "first-order" is used to distinguish first-order theories from higher order theories. In first-order theories (a) predicates may have only individuals as arguments, and are assigned by an interpretation to sets of individuals (b) quantification is allowed only over individuals. Higher order theories may allow (a) predicates having other predicates or functions as arguments, and are assigned by an interpretation to sets of sets, (b) predicate quantifiers or function quantifiers are permitted. ?Philogo (talk) 13:34, 14 January 2011 (UTC)

There are several issues. You might start by reading the SEP article [2]] to get a sense of what is going on. As they say there, "For classical extensional logic (as in this entry), properties can be identified with sets, so that second-order logic provides us with the quantifier “for every set of objects.” The rest of that entry is pretty reasonable. — Carl (CBM · talk) 15:47, 14 January 2011 (UTC)

That article seem to be quite in keeping with the original quote from Mendelson, which was carefully worded. The current version implies that either (a) a predicate may take either another predicate or a set as an argument or (b) that the terms "predicate" and "set" are synonymous. I feel there is a use-mention confusion at the root of this. "a" and "F" are individual and predicate symbols. "a" is not a member of the domain "F" is a not a set of objects in the domain. If "predicate" is just short for "predicate symbol" then predicates are not sets, although predicate sysmbols can be associated with sets. I do not think there is a diasagreement about what is going on rather than a lack of precision in how it is described. I think the original quote from Mendelson was more precise, and less confusing. Philogo (talk) 17:08, 14 January 2011 (UTC)

(1) Of course a predicate can take either a predicate or a set as an argument, assuming that you have a system that has both. For example let Φ(ψ) be the predicate of a predicate ψ which says that ψ holds of exactly one object and let Ζ(s) be a predicate of a set s which says that the number 0 is an element of s.

(2) While predicates and sets are not literally the same, as the SEP article points out, they can be identified when working in classical, extensional logic. In that setting, which is the most common one, we can pass back and forth between a predicate and its extension at will. Therefore, it is common in classical extensional logic to work just with sets, not with both sets and predicates, since having both is redundant. Like I keep saying, it's just a matter of taste.

I don't think I understand what you are trying to say. The original post in this thread was about "propositions", which the article does not mention apart from propositional logic. I can't tell if you are asking about second-order logic, to try to understand it, or if you already understand it and are trying to explain what you want the article to say. — Carl (CBM · talk) 18:15, 14 January 2011 (UTC)

Re This sections heading. The article was edited by Lauri.pirttiaho to say Briefly, first-order logic is distinguished from higher-order logics in that quantification is allowed only over individual variables (but not, for example, over propositions). To settle a bit of an edit-war I altered this to The adjective "first-order" is used to distinguish first-order theories from theories in which there are predicates having other predicates or functions as arguments or in which predicate quantifiers or function quantifiers are permitted or both. citing Mendelson, see under section Lede above. In this section I invited the views of others as to whether quantification over propositions should also be mentioned, see head of this section. (I was not advocating this.) You said 01:33, 12 January 2011 I am OK with the current lede, [my edit] because there really isn't room there to try to go into detail. but subsequently altered the article to read The adjective "first-order" is used to distinguish first-order theories from higher order theories in which there are predicates having other predicates, sets, or functions as arguments or in which predicate, set, or function quantifiers are permitted I am querying, in the politest possibly way, the accuracy and precision of your improvement on Mendelson and whether it improves the article's lede. I feel you were right in your remark of 01:33, 12 January 2011, and your subsequent edit was not "brilliant." but confusing. In any case we cannot fairly attribute it to Mendelson.Philogo (talk) 19:32, 14 January 2011 (UTC)

I still don't follow. The difference between sets and predicates isn't really germane here, but Tkuvho was very insistent on having the word "sets" in the sentence. You two should come to an agreement about it; mathematically it's fine either way. — Carl (CBM · talk) 00:27, 15 January 2011 (UTC)

Yes I know Tkuvho was very insistent on having the word "sets" in the sentence, and I sympathised. That is why I suggested:

The adjective "first-order" is used to distinguish first-order theories from higher order theories. In first-order theories (a) predicates may have only individuals as arguments, and are assigned by an interpretation to sets of individuals (b) quantification is allowed only over individuals. Higher order theories may allow (a) predicates having other predicates or functions as arguments, and are assigned by an interpretation to sets of sets, (b) predicate quantifiers or function quantifiers are permitted. but neither of you commented on that suggestion. Philogo (talk) 00:41, 15 January 2011 (UTC)

There are first-order theories in which predicates may have both individuals, sets of individuals, and other higher-type objects as arguments. For example, all of type theory can be (and often is) formalized as a first-order theory. Second-order arithmetic is a limited version of this, in which there are quantifiers over numbers (individuals), sets of numbers, relations (predicates) on tuples of numbers, and functions from tuples of numbers to numbers. All of that, in a first-order theory.

Moreover, you can have a higher-order theory in which quantification is directly over sets. Instead of having something like (∀ Φ)(Φ(x)) you would have (∀ S)(x ∈ S). In such theories there may be no quantifiers over "predicates" at all, only quantifiers over sets. I think this was Tkuvho's concern, but I can't speak for him or her.

So I don't see that the sentence you are quoting is any less inaccurate than the sentence already in the article. I think this would be better: The adjective "first-order" is used to distinguish first-order logic from higher-order logic. That at least is accurate. There's no way to accurately convey the details of the distinction in a single sentence in the lede of this article. (The article on higher-order logic is also in dire need of attention, I see. But this sort of thing can at least in principle be explained there.) — Carl (CBM · talk) 01:12, 15 January 2011 (UTC)

So is this quote from Mendeson wrong (or just incomplete)

"The adjective "first-order" is used to distinguish first-order theories from higher order theories in which there are predicates having other predicates or functions as arguments or in which predicate quantifiers or function quantifiers are permitted or both.".

I would rather what is said in the lede is the truth if not the whole truth rather than innacurate, so would support your simple The adjective "first-order" is used to distinguish first-order logic from higher-order logic.

It might however be an interesting addition to the article (not in the lede) to outline the limitations of FOL requiring SOL or HOL Philogo (talk) 01:39, 15 January 2011 (UTC) Philogo (talk) 01:39, 15 January 2011 (UTC)

I agree that we should explain it a little more in the article, just not in the lede. The section First-order_logic#Higher-order_logics is intended to do this, and we can work on it. I was just working on higher-order logic, which I didn't know existed (I thought it redirected to second-order logic).

The key point there is that higher-order logic gets extra strength over first-order logic by adding extra quantifiers (which can be simulated in first-order logic) and using standard higher-order semantics (which cannot be simulated with first-order semantics). Just making the syntactic change only results in a strange-looking theory with first-order semantics. — Carl (CBM · talk) 02:01, 15 January 2011 (UTC)

If you look under the section "lede" above I pointed out the incompatibility between the characterisation of higher-order logic in the lede of this article with that given in higher-order logic. To resolve a bit of an edit war I quoted Mendelson, but you think he was wrong/incomplete. Are we agreed to say in the lede to this article, as you suggest, just The adjective "first-order" is used to distinguish first-order logic from higher-order logic.Philogo (talk) 02:31, 15 January 2011 (UTC)

Yes, I agree. I don't think Mendelson was "wrong", that would be too much to claim. I could accept incomplete. It's not just the addition of extra quantifiers, but also the use of standard semantics, that distinguishes higher-order logic. If you take the semantics for granted, then the remaining distinction is the extra quantifiers. But there are plenty of theories that have the extra quantifiers but still use first-order semantics. — Carl (CBM · talk) 02:45, 15 January 2011 (UTC)

limitations of FOL

I have suggested that it might however be an interesting addition to the article (not in the lede) to outline the limitations of FOL - requiring SOL or HOL or other. I would hazard that most student of Logic do not progress further than FOL, and are left with the impression that most everything can be analysed away into FOL. (Quine himslef claimes SOL was set theory in sheeps cloating) This might include (a) analysis of sentences involving adverbs and (b) sentences like the famous "Some critics only admire one one another". I have no objections to examples from mathematics but not think they should be resticted to mathematical examples. It would help if any maths examples were not too technical, since (I assume) our intended reader is not necessarily a mathematician. Philogo (talk) 03:12, 15 January 2011 (UTC)

One thing to keep in mind with "some critics only admire each other" is that the definition of "nonfirstorderizable" is very specific. You could easily formalize that sentence in a theory of first-order logic that has variables for critics and variables for sets of critics, but that is explicitly not permitted by the definition of "nonfirstorderizable". So it's the restriction to single sorted first order logic that is actually being made, but this is not always made clear in the literature. It does not actually require second-order logic to formalize the sentence, just an extra sort for sets of critics, which can be done in first-order logic equally well. When Boolos says "second-order variable" this does not actually imply second-order logic, it just implies a sort of variable that is intended to range over sets, as in the first-order theory second-order arithmetic. — Carl (CBM · talk) 03:23, 15 January 2011 (UTC)

What did Quine mean exactly when he said that first order logic is set theory in sheep's clothing? When I first heard this I assumed that he means that defining variables to range over sets so as to be able to express otherwise second-order statements in first-order logic, is cheating (hence "sheep's clothing). But perhaps that's not what he meant? Tkuvho (talk) 19:35, 15 January 2011 (UTC)

It's second- and higher-order logic that Quine described that way. He was referring to the fact that, in the standard second-order semantics, a quantifier over sets of individuals ranges over all sets of individuals in the metatheory. Therefore, whether a particular sentence is true can depend on the set-theoretic assumptions that are made in the metatheory. That is, the question of which sentences are logically valid will depend on the underlying model of set theory that is used to define the semantics.

For example, there is a (complicated) sentence in second-order logic which asserts that every real number is constructible. This sentence is a second-order logical validity if, in the metatheory, every real number is constructible; otherwise the sentence is unsatisfiable in second-order logic. Now the question whether every real number is constructible is independent of ZFC, which means that we cannot prove in ZFC that this sentence is a logical validity in second-order logic, if it is, and cannot prove it is not, if it isn't. So just the question of deciding logical validity in second-order logic requires being able to decide things that cannot be decided by ZFC.

This is in contrast to first-order logic, where a sentence is logically valid if and only if it is provable, and testing provability only requires quantifying over the set of all possible finite proofs. So as soon as we think that we know what a "finite sequence of formulas" is, we don't need any more set theory to do first-order logic.

From Quine's point of view, a key aspect of a "logic" is that is has a minimal amount of ontology associated. From that viewpoint, it's OK to assume you can quantify over finite proofs, since you are already committed to formulas and proofs are just finite lists of formulas. But Quine would say that you shouldn't have to worry about quantifying over the powerset of the natural numbers just to decide whether some individual formula is logically valid (which, as above, can be necessary in second-order logic). To those who emphasize the finitistic nature of logic, second-order logic isn't really "logic", it's just a disguised way of studying set theory, because the semantics are so dependent on questions of set theory. Hence "set theory in sheep's clothing".

Boolos was an advocate of second-order logic, however, and Shapiro has also argued against Quine's viewpoint. Shapiro's argument (very roughly) is that there are different uses for logic, and that although there is a tradeoff between the finitistic nature of first-order logic and the expressiveness of second-order logic, both deserve to be called "logic" because both are useful for their own purposes. — Carl (CBM · talk) 20:29, 15 January 2011 (UTC)

Thanks, that's a very clear explanation. I gather I believed Quine to say the opposite of what he actually said :) Tkuvho (talk) 21:16, 15 January 2011 (UTC)

Created new section First-order logic#Limitations of First-order Logic

I added a part on expressiveness. I also moved the section above the "extensions" section, since this section is a sort of motivation for that material. It's nice that this is right after the material on Lindstrom's theorem. I think the progression works well. — Carl (CBM · talk) 01:56, 16 January 2011 (UTC)

At top of 'Formalizing natural languages' you have changed the quote from Gamut but kept the citation (which is hecne now erroneous. The examples following are from Gamut 1991, (although not in smae format) so we should mention Gamut 1991, even if we are not keeping the quotation.Philogo (talk) 04:05, 16 January 2011 (UTC)

Under expresiveness, should

• The Löwenheim–Skolem theorem shows that if a first-order theory has any infinite model, then it has infinite models of every cardinality. In particular, no first-order theory with an infinite can be categorical.

be

• The Löwenheim–Skolem theorem shows that if a first-order theory has any infinite model, then it has infinite models of every cardinality. In particular, no first-order theory with an infinite model can be categorical.Philogo (talk) 04:15, 16 January 2011 (UTC)

Terms: individual constants

I see no mention of individual constants in First-order logic#Terms. Why is this? cf Non-logical symbol : "The non-logical symbols of a language of first-order logic consist of predicates and individual constants." Philogo (talk) 00:08, 13 February 2011 (UTC)

If you look just higher up, the article uses the convention that constant symbols are 0-ary function symbols, and so individual constant symbols are covered by the second formation rule, as they are simply function symbols of 0 variables. Are you being coy about that? In any case, I added a sentence to the second formation rule in the terms section, but it was already correct as it stood. — Carl (CBM · talk) 00:23, 13 February 2011 (UTC)

Not coy, just a bit thick perhaps. You mean "A function symbol, with some valence greater than or equal to 0." covers it. A bit like a sentential letter being covered by a "predicate letter of valence 0." I am familiar with latter but not the former. Thanks for enlightening me and clarifying the article for others who may be equally thick or out of date!. I was helping another editor who was wondering what corresponded to names in FOPL. I said 'individual constants' and gave him/her a link to this article only to discover there it wasn't. The answer now must be that names are representable by functions of variance-0. Philogo (talk) 01:46, 13 February 2011 (UTC)

Adding a note to the article about little things like that is always a good idea, I just wasn't sure if that was what you meant or if there was something else you were looking for. — Carl (CBM · talk) 02:09, 13 February 2011 (UTC)

If you look at Wikipedia:WikiProject Logic/Standards for notation#Common basis for syntax and semantics: non-logical symbol and individual constant, constant, (individual) constant symbol, constant symbol constant this convention is not mentioned. (PS Not meaning to (a) nit pick (b) be coy [I am collecting your characterizations of me]). Philogos (talk) 02:27, 13 February 2011 (UTC)

For better or worse I have never looked at that page much. I see it does mention "arity ≥ 0" for function symbols. But overall I don't have any idea whether it matches with our actual practice in articles. — Carl (CBM · talk) 02:34, 13 February 2011 (UTC)

The purpose of the page is to promote a consistent terminology across Logic articles, both those maintained by WikiProject Maths and WikiProject Logic. If you feel this is a worthy aim please edit! E.g. should we drop well-formed formula in favour of formula? Imagine if you would reader new to the field going from one article to the other finding the terms used keep shifting. — Philogos (talk) 02:45, 13 February 2011 (UTC)

I guess it may have been me who added "predicate symbol (arity ≥0)". In that case I thought it was obviously implied that predicate symbols of arity 0 are constant symbols. But I see how that can be confusing to everybody who is not trained in seeing trivial special cases of definitions and arguments. Hans Adler 23:29, 13 February 2011 (UTC)

A nullary predicate symbol is simply a representation of Truth or Falsehood--they are the only nullary predicates. If you included the symbol "T" for Truth, it would be a "logical constant" in the same sense that the symbols for disjunction, negation, and the existential and universal quantifiers are logical constants: their meanings are always the same. Adding a symbol for truth is optional, since for any formula P we can use P->P as a proxy for T. It would also be a "logical constant" in the literal sense of a predicate that always takes the same (logical) value (True)--unlike the other "logical constants" listed (aka "logical symbols"). So when you say "constant symbol" there are two parsings of the expression:

a symbol possessed of constant meaning (like the negation symbol), or a (function) symbol intended to represent a fixed individual, or in the instant case, a (predicate) symbol intended to represent a fixed logical value. Including T as a nullary connective or a nullary predicate symbol is much like including "=" among the logical symbols and the properties of identity among the logical axioms or viewing it as a non-logical symbol--either choice will have an equivalent formalism that does it the other way, so neither is "correct".

There is nothing wrong with having lots of nullary predicate symbols, analogous to the atoms (urelements) of NBG. It might be useful in developing formalisms including notions like time and trust. Lewis Goudy (talk) 14:22, 31 May 2022 (UTC)

First-order language

Redirects here, so this paper, also as (pre)print, specifically, the giant theorem 1.1, which pieces together several (famous) results should probably be mentioned. I'm adding it to further reading for now. (I discovered it while I was looking for an accessible formulation of Kamp's theorem to add at Temporal logic). Tijfo098 (talk) 23:17, 20 April 2011 (UTC)

I don't think there is a section now where that would fit. The idea of first-order definable languages on words is a pretty specialized application of first-order logic (similarly to the way that results on definability in o-minimal structures are a specialized case of general first-order definability). I think that characterizations of languages in computability probably belong in more specialized articles, along with results on o-minimality. Even saying what it means for a language to be first-order definable takes a little work. — Carl (CBM · talk) 00:07, 21 April 2011 (UTC)

Ok, I'll create a stub on that at some point. For important classes, like regular language, we have separate articles that cover the many ways to define/characterize them. Tijfo098 (talk) 09:01, 21 April 2011 (UTC)

That seems reasonable. We do have an article on Büchi automaton that should also link to it. — Carl (CBM · talk) 10:42, 21 April 2011 (UTC)

Set Theory and Mathematical Logic

First order logic is used in (or is) the foundation of mathematics, i.e. set theory in the form of ZFC and similar axiom systems. But set theory seems to be ubiquitous in mathematical logic too. Much of mathematical logic seems to be formulated using set theory (naive version), Most proofs of the basic things like compactness I have bumped into use ZFC in a blatant way. Sets, natural numbers, infinity, the notions of cardinality, uncountability, functions, relations, the axiom of choice, etc. Basically the whole package is used.

What is the relation between mathematical logic and Set Theory on a basic level? Can one be formulated at all without some naive version of the other?

How about a little section discussing this? YohanN7 (talk) 20:25, 2 May 2012 (UTC)

I doubt that it is possible to fully separate them. However in practice, one uses vague informal notions (in natural languages like English) to develop the rudimentary formal theories, and then builds on them to get the more elaborate formal theories. Notice that one can do simple logic without knowing anything about: soundness, consistency, completeness, compactness, the Löwenheim–Skolem theorem, etc.. These results which use advanced set theory are not part of first-order logic itself, rather they are part of its meta-theory; that is, they are about first-order logic rather than within it. JRSpriggs (talk) 06:48, 3 May 2012 (UTC)

Theory

There have been a couple edits over this sentence in the lede:

First-order logic with a specified domain of discourse over which the quantified variables range, one or more interpreted predicate letters, and proper axioms involving the interpreted predicate letters, is a first-order theory.

I don't really understand that sentence myself. Is it trying to define a theory? — Carl (CBM · talk) 11:57, 4 May 2012 (UTC)

I agree that the sentence needs to be improved. But 143.167.82.108 (talk · contribs) was trying to say that interpretation has nothing to do with a theory. For example, he would have it that the theory of gravity has nothing to do with why apples fall and the theory of electromagnetism has nothing to do with static electricity. JRSpriggs (talk) 12:40, 4 May 2012 (UTC)

I usually think a theory is just a set of sentences. Separately, many theories have an intended interpretation that motivates their axioms. Could the article say that in two sentences?

One thing I am thinking about is an inconsistent theory (e.g. {0=1, 0≠1}) that is still a theory but has no intended interpretation. — Carl (CBM · talk)

Typo

Typo: In section "Loving Relations", the formula for 'no rows are empty' should read: ∀y∃xLxy. Simon.

I don’t think so, rows in the tables correspond to the first argument of the L predicate.—Emil J. 14:36, 6 March 2013 (UTC)

Material in predicate calculus / monadic predicate calculus etc.

The organization of and terminology used in material in many related pages is shoddy at best. It's been almost a decade since I've (formally) studied formal logic, but even with that background I found the distinctions both pages made confusing. I figure both pages are important, especially the former, and likely to be visited by relative newbies. I've put this note here so that someone might have the opportunity to amend these pages - unfortunately I won't have time to edit them for a few months. Patrick R (talk) 19:04, 30 March 2013 (UTC)

Vague general criticism is not helpful. Please be specific about what you think should be changed. JRSpriggs (talk) 12:30, 31 March 2013 (UTC)

The article predicate logic is just meant to direct readers to articles about specific logics, but someone had added quit a bit of idiosyncratic stuff there. I pruned it back down. — Carl (CBM · talk) 15:00, 31 March 2013 (UTC)

"There is a fool" example

I think this ambiguity example can be made easier if we also show it the following way. Show that the stronger version is "There is someone (who can be fooled every time)" and the weaker version is "(There is someone who can be fooled) every time". Next, the two versions can be transcribed into different logical statements as in the section. This is exactly how I first understood those paragraphs. FrenzY (talk) 04:03, 29 April 2013 (UTC)

Free and bound variables: Binary connectives

I think in the Binary connectives there is an error, namely:

x is free in (φ → ψ) if and only if x is free in either φ or ψ.

is not true, cause I can e.g. φ(1) → 1 as well as φ(10) → 1 and φ(2) → 2. So φ is dependent on x, but ψ not from x (if I take the ring Z3 (= ring of mod 3)). So it is a one way relation, therefore I don't think you can say anything about the dependencies of ψ reg. to x. There is no relation/connection from ψ to φ defined! It would be if → is a function, but that is not required!

I think the appropriate statement would be

x is free in (φ → ψ) if and only if x is free in φ.

Plus the ongoing sentences... — Preceding unsigned comment added by Laura huber (talk • contribs) 08:42, 14 March 2014 (UTC)

Laura, I am sorry, but what you are saying is nonsense. "x" here stands for any variable (such as y₃ or x₀), not for one of the objects over which the variable might vary (such as 1 or 2). "φ" and "ψ" stand for formulas in the language. "→" is a logical connective, not a function.

The purpose of defining "free" and "bound" variables is to help specify which instances of variables within the scope of a quantifier are being bound by that quantifier. JRSpriggs (talk) 07:00, 15 March 2014 (UTC)

Question about interpreting formula with free variables

The article says: "The most common convention is that a formula with free variables is said to be satisfied by an interpretation if the formula remains true regardless which individuals from the domain of discourse are assigned to its free variables. This has the same effect as saying that a formula is satisfied if and only if its universal closure is satisfied."

However, there is an alternative view, and this concerns the interpretation of quantifier-free formula (QFF), an important class of formulas as many quantifier-free first order theories are decidable. In this view, we say that satisfiability of a QFF is equivalent to satisfiability of the formula in which the variables are all existentially quantified. OTOH, validity of a QFF is equivalent to validity of the formula in which the variables are all universally quantified (see for example Calculus of Computation by Bradley and Manna). Can the main page be changed to reflect this? — Preceding unsigned comment added by Houseofwealth (talk • contribs) 21:10, 13 May 2014 (UTC)

"Satisfiability" is defined as it is to ensure that the rules of inference at List of rules of inference#Rules of classical predicate calculus work. In particular, universal introduction would fail, if your definition were used. JRSpriggs (talk) 10:02, 14 May 2014 (UTC)

Section "Loving relation"

Could anybody please explain to me what is meant by "they are examples" in section First-order logic#Loving relation? I have no idea who is "they" (The individuals a,...,e? The sentences/formulas 1,...,10? The matrices?) and of what they are examples. Thanks in advance. - Jochen Burghardt (talk) 19:00, 18 October 2014 (UTC)

Apparently that sentence meant that all but some diagrams (they are the relations expressed by the diagrams) represent relations. I removed that sentence since it's ambiguous and can be easily be interpreted in a way that it's erroneous. The article needs a major cleanup anyway. Regards. Mario Castelán Castro (talk) 17:44, 19 October 2014 (UTC).

In the removed sentence "Except for the sentences 9 and 10, they are examples.", "they" refers to the diagrams (that is, relations). For sentences 9 & 10, there is only one possible diagram which satisfies those sentences, namely the one shown. For any of the other sentences, there are other diagrams besides the one shown which also satisfy the sentence. Thus the diagram is merely an example in those cases, not a definitive representation of the sentence. JRSpriggs (talk) 10:52, 20 October 2014 (UTC)

@Mario Castelán Castro: each diagram represents a relation. I agree the article needs a cleanup; for example, the "Loving relations" subsection (I didn't read much beyond it) should be in section "Semantics", not in "Syntax".
@JRSpriggs: Thanks, now I understand. Moreover, "satisfy" is more accurate than "represent" (used in the article). Maybe, we should give more than one example diagram, perhaps even a counter-example, at least for some formulas (e.g. for 2 and 3 to illustrate that different quantifiers may not be swapped). And we could note that all diagrams happen to be "minimal" (whitening any red cell in any diagram makes it non-satisying its formula). And to be quibbling, not just 10, but infinitely many formulas can be built from quantifiers and L alone (e.g.∀w∃x∀y∃z Lxy), although with no more than 8 different meanings. - Jochen Burghardt (talk) 06:11, 21 October 2014 (UTC)

To Jochen Burghardt: I like your suggested changes. JRSpriggs (talk) 06:38, 21 October 2014 (UTC)

I started to implement the above suggestions. However, I'm afraid that the text after the diagrams is rather confusing, and so is the extra diagram "2'". Any comments are appreciated. — Maybe we should also show formulas including negation (e.g. ¬∃x L(x,b) = "Nobody loves b") to avoid the impression that changing a white cell to red always preserves the model property.
As another suggestion, what about merging the sections First-order logic#Syntax and First-order logic#Semantics in the long run? The introduction of e.g. a logical connective is easier to understand if it is accompanied by an explanation of its purpose (and an example). In any case, the "Loving relations" section should eventually be moved after the semantics section. - Jochen Burghardt (talk) 17:19, 21 October 2014 (UTC)

Hi! I tinkered a bit with the section and hope I did not introduce some flaw like last time which has been corrected by JRSpriggs - Thanks! Please, improve, or in case you totally dislike it: revert it. I did not deal with the suggestions of relocating or merging. My prima vista opinion on introducing more examples -with negations- is: reserved. This might get still more lengthy in trivialities. Best regards. Purgy (talk) 12:23, 10 December 2014 (UTC)

Ambiguity

The sentence "First order logic is distinguished from propositional logic by its use of quantified variables" is ambiguous. — Preceding unsigned comment added by 109.154.238.115 (talk) 09:18, 21 October 2014 (UTC)

Different symbol in "Validity, satisfiability, and logical consequence"

The first line of that section contains the symbol for phi in text ("...M satisfies φ...") and then a formula in LaTeX. The phi in LaTeX renders differently for me (only for me or for everyone?). So one time it's variant a of small phi and then it's variant b (see Phi). That might be confusing, because it almost looks like a different symbol. One solution would be to use \varphi instead of \phi in LaTeX. But I don't know about the Wikipedia guidlines here and whether you even consider this a problem. (It did confuse me until I realized) Cptwunderlich (talk) 11:23, 29 October 2014 (UTC)

The symbols look different in my browser, too, and they certainly should be made looking similar. I'm not aware of a policy preferring one or the other version; anyway, minimizing confusion should be more important than adhering to (other) style policies. - Jochen Burghardt (talk) 12:12, 29 October 2014 (UTC)

Recent change of lede for "undergraduates"

I do not think that these additions reach their intended target. In first reading them I rather experienced those as not connected to the original content and lacking some common background. There are no links to explain the newly introduced -rather vague- notions and perhaps the whole paragraph -amended by suitable links- would be better inserted under the refered to predicate logic. I will not act on this beyond further comments. Purgy (talk) 13:00, 17 February 2015 (UTC)

I agree that the new text rather confuses me: If predicate and propositional logic corresponds to a lower and higher OSI software layer, respectively, then some 'wrapper functionality' for quantification (lower level) should exist in the higher one, but it certainly doesn't. I'm unable to understand the difference between 'informational layer' and 'knowledge layer'; isn't that the same? I don't think the notion pairs 'syntax'/'semantics' and 'form'/'function' are helpful, as both are rather vague and with shifting boundaries (Once a task has been mechanized, it is considered 'formal'; before, it was considered 'functional'; playing chess is an example). The sentence 'Even people who hail ...' is phrased quite insulting, although I don't like desginers, either.

Apart from that, it is a good idea to have some popular (or undergraduate) introductory paragraphs; however I doubt that many undergraduates are familiar with the OSI model, so maybe it's just the wrong analogy. - Jochen Burghardt (talk) 22:17, 18 February 2015 (UTC)

I agree to making Wikipedia's scientific pages more open to non-nerds would be a rewarding topic. But, sorry, these insertions add imho nothing to accessibility. They just reflect an affiliation of the editor to some profession. In looking up the first of the newly given links I found no relevant foundation for the claimed analogies, and as you said, I also do not see any access to FOL made easier to undergraduates. I simply vote for reversion.

Maybe this provokes the editor to give an explanation. Purgy (talk) 11:51, 19 February 2015 (UTC)

Certainly not a verdict, but I do not oppose to the edit of CBM, in essence reverting the contested additions. Purgy (talk) 08:34, 20 February 2015 (UTC)

Single-Sorted First Order Logic

In the section of Expressiveness, subsection Formalizing natural languages, there it is stated that single-sorted first order logic cannot express many natural language features. Here single-sorted is used for the first time and left unexplained. — Preceding unsigned comment added by 37.4.86.141 (talk) 11:41, 2 June 2015 (UTC)

Being brought to the section =Limitations= by your pointing to an obvious deficit, I allow myself to articulate strong reservations in connecting formal languages with natural languages in the way it is handled in this section. I cannot see how the term natural languages is made available to a formal treatment. I feel the need of someone appropriately knowledgeable to improve this section. Run of the mill linguists may lack intimate experience with formal languages and their possibilities of being incomplete. Purgy (talk) 09:58, 3 June 2015 (UTC)

Recent edits by 72.251.70.97 ...

... have been reverted by Ruud Koot (talk · contribs) calling them style changes. I'm not a native speaker so I have no verdict on this, but I experienced more than a style change in the original edit, and find the reversion not only appropriate but absolutely necessary. I perceived the edits as if FOL were the ultima ratio in logic. Please, 72.251.70.97, discuss your intentions. Purgy (talk) 09:32, 8 June 2015 (UTC)

Lead is messy

@DIY Editor: You are right, the lead is messy. The reason is: First-order logic was merged with Predicate logic recently, and I tried to adapt the lead to discuss the relations between both. However, mentioning all subtleties that came to my mind made the text too long and complicated. Maybe, major parts of it should eventually be moved to an own section, called e.g. "Naming conventions and relations to other logics". On the other hand, at least the article and redirect names, i.e. "First-order logic" and "Predicate logic" should be introduced in the lead, and the former needs to be contrasted with "higher-order logic", and the latter with "propositional logic", so all the mess needs to be in the lead, doesn't it? Currently, I have no idea how to cope with this. Maybe, you have? - Jochen Burghardt (talk) 14:03, 6 December 2016 (UTC)

I don't think that the lede is the place to try to talk about higher-order logic; this is already in a section in the article. Similarly, the article section "introduction" mentions propositional logic. In general, the lede should just be a short summary of the article, rather than developing significant points on its own. — Carl (CBM · talk) 15:12, 6 December 2016 (UTC)

Question regarding an edit

I undid an edit by an IP editor but it may have been a little hasty. I was partly reacting to the edit summary's misspelling of grammar and on second look I'm not sure it wasn't a legitimate edit. The edit changed "there exists a man such as X is Socrates and X is a man" to "there exists X such that X is Socrates and X is a man" which actually seems like it's correct to me. I'll leave this up to someone familiar with the topic of the article. —DIY Editor (talk) 16:14, 11 December 2016 (UTC)

It should be "such that" - I'll fix it. Thanks for the note here, I would not have noticed the edit otherwise. — Carl (CBM · talk) 16:35, 11 December 2016 (UTC)

As a user of English only in non-native ways I do not dare to touch such delicate equipment, but may I remark that the formulation as of now is not very easy to grasp for me (and never was in any of the previous three versions). As far as I understand, it is about the difference between propositions formulated with and without variables (X). I imagine that it might be possible to express this still more amenable to non-precognizant readers. Thank you. -Purgy (talk) 17:43, 11 December 2016 (UTC)

Loving relation

Back in December, I removed a section "Loving relation" which was both overly pedagogical and badly written. It had a number of confusing diagrams. The section was restored today, mysteriously, in a kind of drive-by IP edit. I removed it again, but I wanted to open a section on the talk page to discuss it. Personally, I think that there is no way to make it clear without making it even more laborious and pedagogical. I also do not see a strong motivation for the "Hasse diagram" that was there. — Carl (CBM · talk) 21:08, 23 March 2017 (UTC)

The overly pedagogical tone is probably on my account (see revision history 14 -23 Oct 2014) - sorry for that.

However, I think a lot of logic notions can be exemplified on those examples: universal/existential quantifiers, importance of ∀∃ order, structure (including domain of discourse), a structure satisfying a formula, semantic consequence, and even (non-)categoricity of a formula. I don't know better a example to illustrate those notions to non-experts.

For this reason, I'd like to keep some form of the example (although the recent re-insention wasn't done by me), even if it may need rephrasing and shortening. If there is another article on first-order logic, in a lower-level introductory style, the example may better fit there; but I'm not aware one.

Considering the section structure of the article, "Loving relation" shouldn't be a subsection of "Example: ordered abelian groups", and the latter, in turn, shouldn't be a subsection of "Syntax". Major examples shouldn't be given before section "Semantics", since the purpose of a particular logical formula can't be explained before there. Maybe we should make running examples, with e.g. (using loving relations and ordered abelian groups):

"For example, ∃y L(x,y) is a formula; $\forall x\forall yx+y=y+x$ is another one, using infix notation."

in section "Formulas", and

"x occurs free in ∃y L(x,y), and y occurs bound in that formula."

in section "Free and bound variables", etc. This way, the loving relations example would be spread across the article, its pedagogial tone could be avoided, and probably not all pictures needed to be shown (2. and 4. would suffice to illustrate all above-mentioned notions). - Jochen Burghardt (talk) 11:14, 24 March 2017 (UTC)

Having a running example seems reasonable. Of course, the "L" would only be "love" when talking about a particular interpretation. The section on Abelian groups is purely about the syntax - free and bound variables, etc., without any models, which makes sense because it is in the broader section on syntax. The previous material on the Loving relation was a mixture of an example of a model and some commentary on rearranging quantifiers. The former part might be reasonable as an example somewhere, but I am not sure the latter part is significant enough for the article, which is quite long as is. — Carl (CBM · talk) 11:54, 24 March 2017 (UTC)

The Loving Relation was introduced on 03.03.2012 as an import from the WPDE, and already then did not convince CBM :) . In my last contact, 4.5 years later, I saw it quite expanded in length, and its not rendering well on a tablet caused my attempt to reformat the tables.

Honestly, I like this content within the article, and I am not shooed away by the -admittedly- highly pedagogic style, I would even miss the Hasse diagram, nicely showing the ordering structure in some Boolean lattice.

However, I am far from even commenting on a final decision to leave that example out of this article, or to reinsert it, I am just depositing my personal impressions. Jochen Burghardt's suggestion pleases me very much, also. I am not involved in the reinsertion, too. -Purgy (talk) 14:22, 24 March 2017 (UTC)

An error in the definition of formulas

An example of formulas speaks about a function symbol, althought function symbols are not defined in Formulas section.

Something is wrong! --VictorPorton (talk) 01:54, 8 November 2019 (UTC)

Formulas may contain terms and those terms may contain function symbols. JRSpriggs (talk) 09:44, 8 November 2019 (UTC)

Precedence order (section 2.2.3 Notational conventions)

The section Notational conventions gives an order of precedence, but provides no source for this. I have been looking around, and I can find several sources (presentations from classes mainly), that seem to disagree. This answer from stackexchange quotes Herbert Enderton, A Mathematical Introduction to Logic, page 78, which also has quantifiers with higher precedence than ∧ and ∨. --Lasse Hillerøe Petersen (talk) 13:25, 3 May 2020 (UTC)

If omitting a pair of parentheses would result in two or more reasonable interpretations of the string, then they should be retained. JRSpriggs (talk) 19:42, 3 May 2020 (UTC)

Inconsistency of terminology

There is an inconsistency of terminology between some different articles and I'm not sure how it should be fixed. This article currently has a section called Deductive systems, and it gives as examples of deductive systems, Hilbert-style deductive systems, natural deduction, the sequent calculus, the tableaux method, and resolution. The article on Formal system gives first order predicate logic as an example of a deductive system, i.e. it is a broader definition that potentially encompasses an entire logic. The article on proof calculus, or proof system lists things like Hilbert systems, natural deduction systems, sequent calculus, etc., as examples of proof calculi. So, is a deductive system a logic, or is it a proof system? Or is it not synonymous with either? Or is the terminology just inconsistent among different authors? Dezaxa (talk) 21:31, 29 September 2021 (UTC)

I believe first-order logic is not a deductive system, since the objects of a proof calculus are what are called deductions and intended to formalize deductions. A deduction is like a parse tree of the proven formula, it shows explicitly how the formula is constructed from the axioms via rules intended to preserve truth. But the parse tree of a formula in first-order logic doesn't deduce anything (about truth). C7XWiki (talk) 10:25, 25 September 2022 (UTC)

Example of definable functions

I would like to add function application to the abelian group example, as I think it would make the ability of FOL to apply functions more clear. For example we can construct a formula φ(x,y) that's true iff y = x + x + x, so we can said to have defined f(x) = x + x + x. Some formula such as $\forall x(x\leq f(x))$ makes sense in this context even though f isn't a function symbol in the language, since we read this as $\forall x\exists y(\phi (x,y)\land x\leq y)$. But I don't have proper sourcing to write this section, this book by K. Kunen gives a similar example of how we read function expressions within a formula for "$S(y)\in x$" but not the general case, nor "$f(x)=y$". C7XWiki (talk)

Edit: Maybe Quine 1940 is another sufficient source. C7XWiki (talk) 18:48, 28 July 2023 (UTC)

First Example is incorrect

The introduction to this article is incorrect. It states: "First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable."

First, "Socrates is a man" is not existentially quantified, it is a simple predicate: "x is a man", which is symbolized as "Mx" where M[φ] =df "φ is a man", and x =df a variable (note: Socrates is not a variable, it is a single term "s"). So, "Socrates is a man" would be symbolized as "Ms," not ∃x(Mx & Sx), or "there exists an x such that x is a man and x is Socrates".

Second, the source for this sentence even confirms this:

"First order logic allows the use of sentences that contain variables. So that rather than the proposition

Socrates is a man

one can have sentences of the form

X is a man

where X is a variable."

This explanation doesn't contain any quantifications and merely confirms the use of predicates in first-order logic.

If you wanted to display quantification and predication as an example, the ole "All men are mortal; Socrates is a man; therefore, Socrates is mortal" might make more sense:

1. ∀x(Mx → Ox)

2. Ms

3. /Os

Where: O[φ] =df φ is mortal. M[φ] =df φ is a man. s = Socrates.

Translated out, it would read:

1. For all x, if x is a man, then x is mortal.

2. Socrates is a man.

3. Therefore, Socrates is mortal. 173.13.91.9 (talk) 15:04, 6 July 2023 (UTC)

I completely agree. Do you have a particular text suggestion how the (2nd sentence of the) introductory paragraph should look like? - Jochen Burghardt (talk) 16:13, 6 July 2023 (UTC)

Perhaps something like: "First-order logic uses predicates and quantifiers (among other systems) to extend atomic propositional statements with variables. Whereas "all men are mortal" would be translated as "M → O" or "if you're a man, then you're mortal" in simple propositional logic, first-order logic can express the statement as "∀x(Mx → Ox)" or "for all x, if x is a man, then x is mortal." 173.13.91.9 (talk) 15:06, 7 July 2023 (UTC)

First-Order Sentence definition

According to my understanding a first-order sentence (or just sentence) is defined by not having any free variables. In the article it is stated that a formula is called a sentence when there are no free variable occurrences, specifically: "A formula in first-order logic with no free variable occurrences is called a first-order sentence.".

Does that imply that if we have only one occurrence of a variable to be free (but is bound in the whole formula), the formula is no valid sentence?

If not, it would be good to remove the word "occurrences" in the definition. Dark.Rider85 (talk) 07:32, 31 July 2023 (UTC)

"Free" and "bound" are not predicates that apply to variable symbols, like $x$, but to particular occurrences of variable symbols, e.g. the first and second occurrence of $x$ in the formula $p(x)\land \exists x.q(x)$ is free and bound, respectively. Therefore, your question doesn't make sense, imo (or maybe, I didn't understand it properly?).

On the other hand, I'm not sure that the distinction "sentence" / "formula" is made consistently throughout the article. For example First-order logic ... allows the use of sentences that contain variables in the lead's 2nd sentence could as well be generalized to First-order logic ... allows the use of formulas that contain variables. I didn't check the rest, but I noticed that "sentence" is often used to refer to a natural language sentence, which is a possible source of confusion, but maybe unavoidable. - Jochen Burghardt (talk) 08:38, 31 July 2023 (UTC)

Syntax-semantics distinction and history

Would it help to include some information on the history of the syntax-semantics distinction? (E.g. according to Ebbinghaus's Ernst Zermelo (2007), pp.182--183, acceptance of it was what set "classic" set theory researchers such as Zermelo and Fraenkel apart from the younger generation of set theory researchers such as Goedel, Skolem, and von Neumann). In this way the syntax-semantics distinction appears much more recent than the advent of first-order logic. C7XWiki (talk) 21:23, 20 April 2024 (UTC)

If-then-else

The article currently states:

This definition of a formula does not support defining an if-then-else function ite(c, a, b), where "c" is a condition expressed as a formula, that would return "a" if c is true, and "b" if it is false. This is because both predicates and functions can only accept terms as parameters, but the first parameter is a formula. Some languages built on first-order logic, such as SMT-LIB 2.0, add this.

I don't understand what this is trying to say. Is it trying to say that one can extend first-order logic with if-then-else, and get a (meta-)theory that is still equivalent to first-order logic? This seems incorrect at first blush: ite(P, P, Q) with P as a predicate corresponds to "the simplest second-order sentence admitting a nontrivial model", if I understand the article on second-order logic correctly. But if the extension of first-order logic with ite yields second-order logic, then why not come out and say that? Maybe the result is something else entirely? If so, what is that? Does it have a name? Are all such extensions equivalent/isomorphic to SMTLIB-2.0 or are there non-equivalent extensions? What, exactly, is the above paragraph trying to say? 84.15.176.27 (talk) 10:35, 18 June 2024 (UTC)

It seems rather odd to me too. If C, A and B are propositional variables then $ite(C,A,B)$ is equivalent to $(C\rightarrow A)\wedge (\neg C\rightarrow B)$ which is a well-defined truth function. Dezaxa (talk) 15:19, 18 June 2024 (UTC)

I removed the statement on if-then-else for now; in my opinion it is certainly misplaced in the paragraphs defining formulas (there are many extensions that are not supported, why highlight this one), and it is confusing at least to the posters in this section and to me. Felix QW (talk) 19:31, 18 June 2024 (UTC)

Comment: I think this paragraph referred to expressions like ite(x>0, x, -x) that are known from programming languages, e.g. (x>0 ? x : -x) can be used in C to denote the absolute value of x. See Ternary conditional operator for details in many programming languages. Such expressions, however, do not fit into the scheme of terms admitted by first-order logic. - Jochen Burghardt (talk) 05:00, 19 June 2024 (UTC)