Talk:First-order logic

Older discussion on this page has been archived.

Can we use the word "set" in the vocabulary section?

"A set of predicate variables (or relations) each with some valence (or arity) ≥1, which are often denoted by uppercase letters P, Q, R,... ."

Like the above statement, the vocabulary section of this article keeps using the expression "a set of" in defining concepts such as predicate variable and constant. But what does a set mean in this context? What is the definition of it? Isn't it a concept of ZFC (or other equivalent 1st order theories) which is again dependent on the 1st order logic? I'm worried if it is a circular definition. --Acepectif 06:50, 5 May 2007 (UTC)

Yes, it is somewhat circular, but that is the way foundational mathematics is done, and it is not Wikipedia's task to correct that. Historically, Hilbert's program tried to find a non-circular way to formalise mathematical reasoning, but this hope was shattered by Gödel's incompleteness theorem and related discoveries in the 1930s. Today most mathematicians would probably say one may well conduct a mathematical argument without first having formalised the process of arguing mathematically, and it is only the formalisation that needs set theory. Or, a bit more provocatively, at its root it is merely an article of faith that mathematics works at all. –Henning Makholm 08:43, 5 May 2007 (UTC)

After further thought, perhaps it would be good for the article to say that first-order logic is but a mathematical model of the process of reasoning mathematically, and is not identical to mathematical reasoning itself. It is a very good model, which captures quite accurately which kinds of arguments most real mathematicians will accept as valid proofs. But mathematicians are in general capable of forming those judgements without translating the purported proof into first-order logic, and it is often possible to get at least master's degrees in mathematics without ever having seen the precise rules of first-order logic in a classroom setting. If only I knew how to say that succinctly in the article without sounding to POVish and argumentative ... –Henning Makholm 21:15, 6 May 2007 (UTC)

Algorithm for generating axiom or checking them?

The article says:

When the set of axioms is infinite, it is required that there be an algorithm which can decide for a given well-formed formula whether or not it is an axiom. There should also be an algorithm which can decide whether a given application of an inference rule is correct or not.

I thought the correct statement would be:

When the set of axioms is infinite, it is required that there be an algorithm which can generate all axioms by recurring application, so that each axiom can be generated in a finite number of steps. The same is true for inference rules. For each inference rule there should be an algorithm which implements it, so that each implementation can be carried out in finite number of steps.

Any comments? Dan Gluck 15:34, 11 July 2007 (UTC)

Actually, no algorithms are required for general first-order theories. I don't know how everyone missed that. For example the full theory of any first-order structure is a first-order theory, but in most cases there is no way to decide whether a given sentence is in there or not, and no way to enumerate the theory. I removed the two sentences from the article. — Carl (CBM · talk) 16:26, 11 July 2007 (UTC)

OK, but still you need an algorithm to generate the axioms, otherwise how do you generate them? In other words, are there any objections for me adding the paragraph I have suggested?Dan Gluck 18:25, 11 July 2007 (UTC)

If you can recognize an axiom algorithmically, you can generate them by generating all finite strings of symbols (for example, in order of increasing length) and filtering out those that are not axioms. Merely requiring that the set of axioms are recursively enumerable is too weak a condition to be of much use; if you don't have an algorithm for deciding whether a formula is an axiom, you won't be able to decide whether a purported proof is valid. –Henning Makholm 19:39, 11 July 2007 (UTC)

Thanks, this is much clearer now. Dan Gluck 06:43, 12 July 2007 (UTC)

Any set of axioms generates a first order theory, whether or not that set is computable or computably enumerable. For example the theory of true arithmetic (the set of sentences of PA true in the standard model of the natural numbers) is a first-order theory but it has no effective axiom system. I would not support adding any claim to the contrary to the article. — Carl (CBM · talk) 20:57, 11 July 2007 (UTC)

That is true. My point was whereas restricting to decidable axiom sets is useful (i.e., one does not have to do it, but it it may be useful in particular applications), there is no good reason to restricting only to recursively enumerable axiom sets. It excludes many of the benefits of assuming decidability, and does not improve the expressivity of the logic; any theory with an r.e. set of axiom has an equivalent (in terms of which formulas are provable) theory with a decidable set of axioms. Though the claims quoted above seem to have disappeared now, I think that for full clarity the article should explicitly say that one often but not always consider theories with the added requirement that axiomness is decidable. –Henning Makholm 21:35, 11 July 2007 (UTC)

We might as well use the standard terminology, though. First-order theories with a decidable language and a decidable set of axioms are called effectively axiomatized in the terminology I am used to. Maybe there are other synonyms. Without an extra modifier, there is no reason to think that a first order theory need be effectively axiomatized, and in fact it won't be in the common case where the theory is a complete, undecidable theory of a particular structure. — Carl (CBM · talk) 21:42, 11 July 2007 (UTC)

I think it depends a lot on the subdiscipline one is working in whether that case is in fact "the common" one. In computer science (whence I come) a theory where the axioms are not decidable would be considered a rather strange one. But I agree that the term "first-order theory" does not in itself imply that it is effectively axiomatized. I'm merely concerned that some readers might not notice that there is no such requirement unless we explicitly note that it is something one can add. –Henning Makholm 22:22, 11 July 2007 (UTC)

This article makes a separation between logical axioms, of first-order logic, and non-logical axioms, of the first order theory one is considering. Your arguments all referred to the non-logical axioms. What about the logical axioms? There are versions with a finite number of such. Is it legitimate to have a version with logical axioms which are not decidable? Dan Gluck 06:43, 12 July 2007 (UTC)

I don't know of any presentation of ordinary first-order logics which has an undecidable set of logical axioms, so it is not clear to me that the question is relevant. I don't see any inescapable reason why one could not define a logic with an undecidable set of logical axioms if one wanted (except for the question of whether the result is useful enough to be called a "logic"). But that logic would be a different logic from the ordinary first-order logic, and therefore not directly relevant to this article. –Henning Makholm 19:54, 12 July 2007 (UTC)

The reason I'm asking is that I think the statements about semidecidability assume semidecidability of the axioms, they do not however assume their decidability. In its present form the article nowhere states anything about these assumptions. Dan Gluck 06:36, 13 July 2007 (UTC)

The article explicitly presents a decidable set of logical axioms for first-order-logic, and mentions that there are other well-known axiomatizations of FOL that would also work. Those other axiomatizations also have decidable sets of locigal axioms; this is fact, not assumption. I don't see what there is to worry about. Which sentence could possibly be relevant in the article that even mentions undecidable sets of logical axioms? Keep in mind that logics with such axiomatizations are not FOL. –Henning Makholm 21:23, 13 July 2007 (UTC)

No, there is nothing called "first order logic" with an undecidable set of logical axioms. But phrases such as "The axioms of first-order theories" uniformly refer to the nonlogical axioms, since the logical axioms are fixed across all first order theories, and in particular a first order theory is usually defined as (the logical consequences of) a set of (nonlogical axioms) in a fixed language, — Carl (CBM · talk) 22:54, 13 July 2007 (UTC)

OK. My point was that the article only gives an example of axiomatization of first-order logic, and while in this one and in any other I ran into the axioms are decidable, I wanted to be sure that this is part of the definition of a first-order logic, i.e. that no one can give axiomatizaion where the axioms are undecidable and call it "first-order logic". You have confirmed that this is indeed the situation. Thanks. Dan Gluck 09:46, 14 July 2007 (UTC)

Quantifier axioms

I can't read the quantifier axioms due to unicode problems, and while I've figured out alone two of them and changed the problematic characters to math formulas, I didn't figure out the other two. Can anyone please change the problematic characters to math formulas? By the way, the second axiom is in fact easily proved from the first one, hence is not an axiom. Dan Gluck 20:50, 11 July 2007 (UTC)

Is this still a problem?--Cronholm¹⁴⁴ 10:06, 16 July 2007 (UTC)

No, thanks.Dan Gluck 11:58, 16 July 2007 (UTC)

Major edit

I've done a major cleanup and added of explanations and examples. Hopefully I haven't done mistakes. Dan Gluck 08:14, 12 July 2007 (UTC)

This Explanation Sounds Backward, Please Explain

74.229.250.5 00:55, 24 August 2007 (UTC)==Why is first-order logic needed?== Propositional logic is not adequate for formalizing valid arguments that rely on the internal structure of the propositions involved. For example, a translation of the valid argument All men are mortal Socrates is a man Therefore, Socrates is mortal into propositional logic yields A B $\Rightarrow$ C which is invalid ($\Rightarrow$ means "therefore"). The rest of the article explains how FOL is able to handle these sorts of arguments.

This is at the top of the article and the symbols seems to describe the syllogism correctly. But then the last sentence says "which is invalid ($\Rightarrow$ means "therefore")." I guess the reader is supposed to see something wrong here, but the sentence doesn't tell us what that might be. Why does it point out the arrow means "therefore"? Is the arrow a problem? It would seem not, because "THEREFORE, Socrates is mortal" is the correct end of the cogent syllogism. This leaves the reader wondering, "What exactly is the problem FOL solves that propositional logic can't?".

I tried to explain it. Is it better now? Dan Gluck 08:34, 16 July 2007 (UTC)

I think it is better. I may try to rephrase a little, but the emphasis on the structure of the formulas is much better now. — Carl (CBM · talk) 18:59, 16 July 2007 (UTC)

rjm Aug 23, 2007 I believe it would help to simply state that "propositional logic reqeuires the content of the syllogism be replaced by generic symbols, thus losing the logical connections between the premises. Therefore, propositional logic is unsatisfactory in many such cases." I too had to read the section multiple times to understand why you seemed to be calling the most famous valid syllogism invalid. Clarify that the invalid syllogism is the one with just letters, not the original one about Socrates. Reading the first comment here helped me, but that shouldn't be necessary. rjm Aug 23, 2007

I was taught that $\Rightarrow$ is the predicate calculus dyadic operator implies which has its own truth table; I don't thing referring to it as therefore emphasises this formality. -- Mickraus 11:37, 14 September 2007 (UTC)

Clarity of variable use

In the second paragraph the construction of two propositions within FOL is explained thus:

"In propositional logic these will be two unrelated propositions, denoted for example as p and q. In first-order logic we may denote both as: Man(x), where Man(x) means that x is a man. For x=Socrates we get the first proposition, and for x=Plato we get the second one."

While in mathematics 'x', used as a variable, can be used to denote any element in the context, this is both inconsistent with how variables have been used in the entire history of logic and also how they are in contemporary use. Suggest a change to Man(x) and Man(y) for x= socrates and y=plato.

Given that the full propositional form of just these simple sentences is something like (Ex)Man(x)& Socrates(x) and (Ey)Man(y)& Plato(y) respectively, it is little wonder that this convention has been maintained over the years. It maintains clarity and allows for manipulation of the domain that may not be possible otherwise.

Wireless 143.252.80.100 09:32, 22 August 2007 (UTC)

The whole point was to explain that in Man(x) every consant can replace x. You current suggestion is not beneficial for such an explanation. However, you are invited to suggest other options.Dan Gluck 11:51, 22 August 2007 (UTC)

If you mean that the predicate 'Man' can be applied to every non-logical constant x,y,z... then fine. But 'Man(x)' alone is not a proposition in FOL as is claimed. If you don't want to introduce quantifiers at such an early stage, suggest just using words: 'if you substitute Socrates...' and 'if you substitute Plato...'. Otherwise it is plain unclear.

Wireless 143.252.80.100 12:01, 22 August 2007 (UTC)

OK, I change it so that it's clear that Man(x) is a realtion rather than a sentence. Dan Gluck 06:29, 23

August 2007 (UTC)

I've cleaned up the language of that paragraph, hopefully making it a bit clearer, but keeping all the substance. Hope you don't mind. Wireless99 09:23, 23 August 2007 (UTC)

Can we clear up the Modus Ponens paragraph?

First of all, according to ordinary convention, the turnstile symbol is just a symbol for logical consequence in general and therefore does not always mean that the formula following it is a theorem. A formula is only a theorem if it is a logical consequence of the empty set i.e. true under every interpretation. There is no such thing as a "new" theorem.

Also, Modus Ponens(MP) is described rather unclearly. The description suggests that MP ONLY applies to theorems and not to contingent formulae also, which is (i would argue) its most important application (unless you are a mathematician). Would therefore suggest the following:

P; P > Q
  ----
Q

Or the greek equivalent (couldn't transcribe it properly - apologies) Wireless99 15:43, 23 August 2007 (UTC)

This article is indeed math-oriented. There has been an old debate about that, which is located in the archive, from the time when this page was called "predicate calculus". It has been agreed to change the page's name to "first-order logic" and keep it math-oriented, and have the philosophy-oriented stuff in quantification. This seems to me reasonable, and I think (though not sure) that the term "first-order logic" is indeed in use by mathematicians more than by anybody else. If you disagree with the decision, you may start here a new debate. You may otherwise add a remark in the beginning which says something like: This article is mathematically oriented. For philosophically oriented discussion, see quantification.

• As for your other remarks, this symbol: $\vdash$, is in fact in use as a sign that the formula following it is a theorem. See for example Metamath Proof Explorer Home Page.
• You wrote "A formula is only a theorem if it is a logical consequence of the empty set i.e. true under every interpretation." This statement is inaccurate, since the empty set is not a well-formed formula. The correct statement is: "P if and only if for every statement Q, Q implies P". This is not a statement in first-order logic, but rather in second-order logic (it is in fact a theorem of some second-order logics). Another statement, which is a theorem in propositional logic, is "P implies (Q implies P)". While true, this is totally irrelevant, because this is not the way one proves theorems in first-order logic. By the way it is true that in propositional logic you can use truth tables in order to check whether a sentence is a theorem or not, but again this is not how you prove a sentence (in mathematical logic).
• You wrote "There is no such thing as a "new" theorem.". When you are proving theorems in mathematical logic, you do it by some order starting from the axioms and moving on, one step at a time. A "new theorem" in step n is a theorem which is proven in step n; it is of course not new, in the sense that no theorem is new: all the theorems in mathematics are always true (well, actually there's a philosophical debate about that...). If you can describe it more clearly and accurately than what already appears in the article, as you have done successfully in the lead section, you are invited to do that.
• Modus ponens, which has an article of its own, appears here only as an inference rule, in the sense of proving (or creating, depends on your point of view) theorems. As such, your suggestion for changing the way in which it is presented is not appropriate here.

Dan Gluck 20:13, 23 August 2007 (UTC)

Are we talking about the same FOL? In any FOL I am familiar with, the empty set is perfectly well formed and when you write $\vdash$P it is merely shorthand for following on from the empty set, i.e. that P is a logical consequence of the set of no premises (and for the picky mathematicians out there - thats 'set' in the sense of naive set theory as it is used by logicians). Consult any elementary logic textbook. Also, while there may be new mathematical truths, there can be no new logical truths in FOL - these are all given at the start by definiton. Do not let the fact that mathematics may be able to be expressed well in FOL confuse your thinking.

"this is not the way one proves theorems in first-order logic."

Rather, this is the way mathematicians use FOL. The language you are working in is correct and complete, and that you only use a fragment of it and call it "mathematical logic" or whatever is up to you. Wireless99 21:39, 23 August 2007 (UTC)

I'm not interested in arguing about mathematicians, but that section does need to be edited some. Really the whole article needs some work. I'll try to get to it if nobody else does, but I wouldn't argue with almost any rewrite of the modus ponens section. — Carl (CBM · talk) 00:23, 24 August 2007 (UTC)

Wireless - what you write about the empty set sounds vaguely familiar, and since I studied logic many years ago, you may be right. Now, by "new logical theorems" I meant in the sense of, for exampe, automated theorem generators; Of course nobody really needs in practice to "prove" logical theorems, but there is a meaning in doing that: You may start with few axioms and generate all logical theorems by the use of inference rules. Anyway, MP is also used to prove non-logical theorems, as you know. You may change the words "old" and "new" to something more well-suited if you wish. What I DO think should be kept in mind is the use of inference rules to move from one set of theorems to another theorem. It is true that ALL inference rules - including MP - can be used for contingent formulae as well. But I'm not sure that in the context of this article this is a more important use. Dan Gluck 18:52, 28 August 2007 (UTC)

I agree with all that you say above, apart from I would wish to (re)start the debate about the usefulness of focussing on the mathematical uses of FOL. While this debate may be futile given that the logic portal is starting up, this article will most likely become superfluous once the logic portal has gotten going. Either suggest changing title of article to "mathematical and computer science uses of FOL" (or some equivalent) or widen it out to talk of all of FOL proper so it may somehow be usefully included in the portal once it has reached a sufficent level of independence from mathematics/philosophy etc. Wireless99 09:20, 29 August 2007 (UTC)

I don't care if you insert philosophy related perspective, but it seems to me that some separation between this and, say, automated theorem generators perspective (which is more or less the opposite perspective?) should be respected. Given this, both can live at the same article. What do you say? Dan Gluck 14:24, 29 August 2007 (UTC)

I agree. However, I will have to take some time to come up with a "philsophy perspective" and do some research. I was taught FOL within philosophical logic, and so will need some time to separate the two, to be able to write something suitable for the article. Question: does this constitute original research? Wireless99 14:50, 31 August 2007 (UTC)

I don't know, I think it depends on how you write it. Though I studied both mathmatical logic as a part of a degree in mathematics and logic as a part of a degree in philosophy, I never heard about FOL in the philosophy course because it was very low-level. So I don't really know what is the philosophical perspective... maybe I'm just kistaken and there is no such thing, I just encountered an old debate here about this and assumed that there is.

Anyway if you come up with your own idea about what is the distinction and write two different sections, one titled "mathematical viewpoint" and the other "philosophical viewpoint", this may be original research. A solution could be for example to write something mixed, but having for example different section(s) about things like Goedel's theorem and automated theorem generators which seems to me not to occupy much of philosophers' research time (maybe I'm mistaken here again?), and another section(s) about things which philosophers emphsize. Dan Gluck 21:01, 31 August 2007 (UTC)

You are mistaken at least when it comes to Godel. Godel's theorems occupy alot of philosophers time. The incompletetness of any system with the capacity to represent arithmetic is a very significant and puzzling result over which philosophers spend a lot of time. Automated theorem generators are a little more boring for philosophers perhaps, but there are philosophical issues here such as those related to turing machines. I'll have to have a think and see if I can justifiably write a separate section in this article entitled "philosophy". Wireless99 09:42, 1 September 2007 (UTC)

classical mathematics is not all mathematics

The article said: it is generally accepted that all of classical mathematics can be formalized The language of first-order logic has sufficient expressive power for the formalization of virtually all of mathematics. A first-order theory consists of a set of axioms (usually finite or recursively enumerable) and the statements deducible from them. The popular set theory ZFC is an example of a first-order theory, and it is generally accepted that all of classical mathematics can be formalized - in ZFC (in which case, if true, one may drop the qualification 'virtually' from the previous sentence in which it occurs). I deleted the part in the parenthesys, since it says that if classical mathematics can be formalized in ZFC, a first-order theory, then first-order logic has sufficient expressive power for the formalization of ALL of mathematics, implying that classical math is all math! As an example, second-order logic surely canno t be expressed by first-order logic. For the same reason, I'll change "virtually all of mathematics" to "most of mathematics". Dan Gluck 19:47, 24 August 2007 (UTC)

Have you any idea about the relationship between first-order classical set theory and higher-order logic? We're talking about expressing things without making clear what it means to "express" something, but nothing yet has been said about "n-categorically expressing" something for some ordinal n. So what can you express (n-categorically or not, for some ordinal n) in second-order logic that you cannot express in first-order set theory? Nortexoid 07:58, 30 August 2007 (UTC)

You are invited to make it clearer in the article, in a way that even a stupid man like me may understand. Dan Gluck 15:32, 30 August 2007 (UTC)

Why is first-order logic needed? - explaining a revert

I reverted from: Clearly the propositional translation is invalid. Let both A and B be true and C false. This interpretation makes the argument invalid. (Syntactically, it is easily observed that one cannot derive C from A and B in propositional logic.) In order to adequately translate the argument, one would have to pay attention to the content of the statements over and above truth values of the simple propositional constituents.

back to:

This translated argument is invalid: logic proves theorems only according to their structure, and nothing in the structure of this translated argument (from A and B follows C) suggests that it is valid. One would have to pay attention to the content of the statements, which is beyond the scope of logic. Translated into propositional logic, this syllogism has the same structure as a translation of "It is raining; The sun shines; Therefore, 1+1=3".

If you knew anything about the subject you would know that the current revision is rubbish for a number of reasons. First, it says that the argument is *invalid* and then provides a *syntactic* reason for its being so without citing any correspondence between validity and derivability (with respect to some class of deductive systems). Nor is it clear what is meant by "nothing in the structure...suggests that it is valid". What role does 'suggest' play in that sentence? Also, there are deductive systems (generating a set of theorems which is consistent or not) which have as a rule (derived or not) "from A and B, infer C". The rest is very poorly written for a logic article. Certain people need to refrain from editing articles fo a certain nature. Nortexoid 08:01, 27 August 2007 (UTC)

Does the above refer to the current version, or the one or the one when the above paragraph was entirely contained within the article? because there have been some changes. Also, if you feel its that bad, improve it yourself. Wireless99 12:13, 27 August 2007 (UTC)

for the following reasons:

• "clearly" - it is certainly not clear for those unfamiliar with the subject.
• It should be emphasized that logic proves theorems only according to their structure, a thing which most people are unaware of. Noting that "Syntactically" one cannot derive C from A and B, doesn't mean anything to the layman, at least at this stage (beginning) of the article.
• An example is in place, hence the example about the sun shining.

Dan Gluck 20:01, 24 August 2007 (UTC)

I've carried out quite a significant re-write of the section, hopefully its clearer. See what you think. Feel free to revert. Although I'd prefer it, unless you really hate it, that you'd try and improve rather than just flat out revert it :) Wireless99 14:34, 26 August 2007 (UTC)

I really like your edit, perhaps I'll make some slight changes but overall I think it's good. Dan Gluck 21:20, 26 August 2007 (UTC)

Article needs history and etymology

Who coined the term First-order logic, when, where, how, and why? What's First-order logic been used for -- especially has it been used for purposes a general audience can easily appreciate? A long article should have this information, if at all possible. The current article disappoints; like reading a Chess article that jumps directly into chess notation, describing clever plays, without mentioning the game's origins, history, or players. --AC 03:31, 20 September 2007 (UTC)

Limitations of first-order logic

• Section about sorts is unclear.
• Does the fact that graph reachability cannot be expressed in FOL follows from the Löwenheim–Skolem theorem? If indded so, it should be mentioned.

Dan Gluck 08:15, 24 September 2007 (UTC)

Provable Identities

• Can anyone provide the proofs? I am dying to know!