Vaughan Pratt (talk | contribs) |
|||
(2 intermediate revisions by the same user not shown) | |||
Line 311: | Line 311: | ||
Frankly, I'm not quite sure what exactly is your point either. I have been assuming you are objecting to calling "replacement for subformulas" (the principle of) extensionality. This is a terminology issue. I think I've shown above that there are sources calling it that way, and there also sources calling it "replacement rule/principle" as well (which seems more natural to me). You appear to me to think to think otherwise, and say no such rule/principle is mentioned anywhere in those sources, i.e. that I'm misinterpeting all of them. It's not really an important issue with respect to ''this article'', so let's just end this futile conversation. [[User:Tijfo098|Tijfo098]] ([[User talk:Tijfo098|talk]]) 17:50, 30 March 2011 (UTC) |
Frankly, I'm not quite sure what exactly is your point either. I have been assuming you are objecting to calling "replacement for subformulas" (the principle of) extensionality. This is a terminology issue. I think I've shown above that there are sources calling it that way, and there also sources calling it "replacement rule/principle" as well (which seems more natural to me). You appear to me to think to think otherwise, and say no such rule/principle is mentioned anywhere in those sources, i.e. that I'm misinterpeting all of them. It's not really an important issue with respect to ''this article'', so let's just end this futile conversation. [[User:Tijfo098|Tijfo098]] ([[User talk:Tijfo098|talk]]) 17:50, 30 March 2011 (UTC) |
||
==Whole article is based on a false premise== |
|||
There have been so many comments on this page in the past seven days that I thought I would just start a separate section rather than try to answer them individually. |
|||
The article starts out by defining the principle in question to be that "every declarative sentence expressing a proposition (of a theory under inspection) has exactly one truth value, either true or false.[1]" |
|||
It then goes on to say that "A logic satisfying this principle is called a two-valued logic[2] or bivalent logic.[3]" |
|||
Now the problem with this is that [[Boolean algebra]]s are traditionally distinguished from [[Heyting algebra]]s as being the algebra of two-valued logic. This is not the same thing as the "principle of bivalence" if we are to believe the article's definition of the concept. Picture a universe consisting of two places, Paris and London, each with two states, raining (1) or not raining (0). Then the proposition "it is raining" has four truth values, namely 00, 01, 10, and 11, because it can be interpreted in either Paris or London, and for each such interpretation the proposition further has two interpretations, that it is raining or not. |
|||
Nevertheless this proposition is interpretable in a two-valued logic, because there is no question that "either it is raining or it is not raining" (unless you want to quibble over drizzling or snowing). Regardless of whether we are interpreting this proposition in Paris or London (for definiteness, the centre of each say), one or the other possibility must be the case. |
|||
Until the article comes to grips with this issue it must be considered confused. Attempts to fix it are equally confused as long as they don't come to grips with it either. |
|||
The interesting question for Wikipedia is where it wants to position this article. If as a contribution to fuzzy thinking (and Wikipedia is full of such articles, for example the one on the [[greenhouse effect]]) then it is an ideal, even exemplary, candidate. If as a contribution to what [[Ernst Schröder]] called "exakte Logik" however then the sooner it is deleted the better, as there is no obvious logic article to redirect it to. --[[User:Vaughan Pratt|Vaughan Pratt]] ([[User talk:Vaughan Pratt|talk]]) |
Revision as of 05:21, 4 April 2011
This article is of interest to the following WikiProjects: | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
Comment by Brighterorange
I removed the following text:
- The principle of bivalence is intuitionistically provable.
- Define ¬A as (A → contradiction). I.e., a false statement is one from which one can derive a contradiction. This is the standard intuitionistic definition of what it is for a statement to be false.
- So using this definition, if we have (A ∧ ¬A) this can be written as (A ∧ (A → contradiction)) → contradiction.
- So (A ∧ ¬A) → contradiction.
- So ¬ (A ∧ ¬A)
.. because I believe that it is factually incorrect.
- The text before it is contradictory (if a proposition can be truth-valueless in intuitionistic logic, how can the principle be provable?)
- I disagree that ¬A is the same as "A is false." At least from the Martin-Löf perspective, intuitionistic logic is concerned only with judging that propositions are true. Thus, a proof of ¬A must be thought of as a proof that "the negation of A is true". (I don't believe the distinction is pedantic here, since this article is about the meaning of true and false!)
- The article on Bivalence and related laws states that the law of bivalence can not be stated as a proposition
- The proposition given is exactly the statement of the law of noncontradiction, which bivalence is "not to be confused with."
- The statement that is proved does not appear to be, even informally, a propositionized version of the principle of bivalence,
- it is a negative statement and the law of bivalence is positive
- it states a conjunction, while the law of bivalence states a disjunction (Brighterorange 17:17, 14 Apr 2005 (UTC))
- OTOH The principle of bivalence is intuitionistically contradicted: This statement is false.
Confusing article
This article is quite confusing.
The claim is made, also in various other articles, that the Principle must not be confused with the Law of excluded middle, and for deeper insight we are referred to here, so one should hope that the exposition here would clarify things. Unfortunately it doesn't.
What are we to make of this sentence: "A proposition P that is neither true nor false is undecidable." A proposition is not a decision problem, how can it be undecidable? What does it mean that a proposition is neither true nor false?
Then: "In intuitionistic logic, sometimes the truth-value of a proposition P cannot be determined (i.e. P cannot be proved nor disproved)." That happens all the time, doesn't it? What about Goldbach, GRH, and so on? If this sentence should be here at all, it needs to be formulated in a way that the intended meaning shines through.
Then, next sentence: "In such a case, P simply does not have a truth-value. Other logics, e.g. multi-valued logic, may assign P an indeterminate truth-value." This confuses the notion of logic in the sense of a system with proof principles and such that can be used to prove theorems with something that is essentially "just" an algebra (a set with operations).
Two formulations of the Principle are given. The intro has: either P is true or P is false. Later we see: "P is either true or false." Both agree that this is "for any proposition P", but the latter mysteriously adds: "at a given time, in a given respect", making clear (but not to the unsuspecting reader) that we are working in the Aristotelian philosophical tradition here. Apart from that, are these two formulations equivalent? In normal parlance they are, but here we are clearly out of the comfort of normal parlance, and nothing means what it appears to mean anyway.
The subsection entitled Bivalence is deepest claims that it is "not possible to state the principle of bivalence in such a way [i.e., as a propositional formula], as the traditional propositional calculus just assumes sentences are true or false." But why is it not just the conjunction of (the propositional formulas for) Excluded middle and Non-contradiction?
Concerning the status of ⊧P (by which I mean truth instead of provability) we can distinguish three possibilities: (1) we know for certain (by whatever means) that this is the case, (2) we know equally certainly that this is not the case, and (3) we don't know (yet?) one way or another. Likewise for ⊧¬P and ⊧P ∨ ¬P. Altogether 3×3×3 cases. From the article I cannot figure out which of these are compatible with the Principle, and which are excluded by it.
Help. --LambiamTalk 12:44, 3 June 2006 (UTC)
- Unfortunately it seems this confusion is not unique to Wikipedia. ("exclusive disjunction of contradictories" per Suber) sort of looks like "bivalence", but it seems to me, now that we mention it, that we could have a situation where P or not-P is always true, P and not-P is always false, but P and not-P might not be individually true or false. So if the "exclusive disjunction of contradictories" is not "bivalence", then "bivalence" is not formalizable in this way at all. In any case, even if we're not clear on this point, it's pretty clear that some of this article is just wrong. 192.75.48.150 19:11, 29 June 2006 (UTC)
- I'm a bit confused.
If I said "this statement is false" then it can be neither true nor false, how does this work with the law of bivalence?
This is Kleene's (1952) 3-valued logic for the cases when algorithms involving partial recursive functions may not return values, but rather end up with circumstances "u" = undecided. He lets "t" = "true", "f" = "false", "u" = "undecided" and redesigns all the "propositional connectives". Our friend the LoEM appears on queue:
- "We were justified intuitionistically in using the classical 2-valued logic, when where were using the connectives in building primitive and general recursive predicates,since there is a decision procedure for each general recursive predicate; i.e. the law of the excluded middle is proved intuitionistically to apply to general recursive predicates.
- "Now if Q(x) is a partial recursive predicate, there is a decision procedure for Q(x) on its range of definition, so the law of the excluded middle or excluded "third" (saying that, Q(x) is either t or f) applies intuitionistically on the range of definition. But there may be no algorithm for deciding, given x, whether Q(x) is defined or not (e.g. there is none when Q(x) is μyT1( x, x, y )=0 ). Hence it is only classically and not intuitionistically that we have a law of the excluded fourth (saying that, for each x, Q(x) is either t, f, or u).
- "The third "truth value" u is thus not on par with the other two t and f in our theory. Consideration of its status will show that we are limited to a special kind of truth table.
It will take some reading and some time to get the jist of this. Kleene is definitely trying to accommodate the intuitionist viewpoint. The following are his "strong tables" that he says is "not the same as the original 3-valued logic of Lukasiewicz (1920)." (§64, pp. 332-340).
~Q | QVR | R | T | f | u | Q&R | R | T | f | u | Q→R | R | T | f | u | Q=R | R | T | f | u | ||||||
Q | T | f | Q | T | T | T | t | Q | T | T | f | u | Q | T | T | f | u | Q | T | T | f | u | ||||
f | T | f | T | f | u | f | f | f | f | f | T | T | T | f | f | T | u | |||||||||
u | u | u | T | u | u | u | u | f | u | u | T | u | u | u | u | u | u |
wvbaileyWvbailey 22:20, 7 November 2006 (UTC)
A story about Clever Teacher
The story custed by the contingent. A boy caught a butterfly and asked the teacher to answer whether it is alife keeping the insect between his hands. If teacher tells "It is dead", he will let the butterfly to fly away. If teacher tells "It is alife" he will imperceptibly squash the poor insect to fool the teacher otherwise. The wise teacher got to the core of the trap and answered: "Everything is in your hands". Excuse me if it is inappropriate for bivalence. Peahaps it links to the liar paradox, since present state manipulates the future. --Javalenok 11:03, 15 September 2006 (UTC)
On pain of contradiction
- The law of bivalence itself has no analogue in either of these logics: on pain of contradiction, it can be stated only in the metalanguage used to study the aforementioned formal logics.
I thought it was unformalizable, and I'm not surprised that it is so on pain of contradiction, but I'm curious how this is a consequence of the liar paradox. 192.75.48.150 15:09, 15 September 2006 (UTC)
- I think that claim is only good if you accept the Tarski-kind of reasoning that holds that liar-like sentences are meaningful where they occur and so a language containing them can't be a tool for formal study of a language: i.e., that you can't do formal semantics for a natural language. But the principle clearly can be formulated formally, like this: (For all S)(val(S) = T or val(S) = F and not(val(S) = T and val(S)=F). Formulated in certain languages--paradigmatically where "S" ranges over the sentences of the language being used--then a language where you can say this will also be a language where you can formulate a liar paradox. But it's hardly universally agreed that liar paradoxes show something unacceptable about the langauges they are formulated in. There are various ways of arguing that (1) They are grammatical accidents that cannot really be legitimately formed in those languages, or (2) That even of formable as sentences they don't mean anything (not even what they appear to mean), so they don't pose a problem, (the "ungrounded" approach) or that (3) Even if a language has such problematic sentnecs, and they're meaningful, they don't undermine the functioning of the rest of the language (the "relevance" approach).
The difference not well-stated in the article--and which I won't undertake to fix--seems to be that Non-contradiction and Excluded middle are sentences, or patterns of sentences, holding or not holding in a language. Bivalence is a claim about the semantics of a language. They will of course, correspond in certain ways. But the claim at issue takes for granted some more controversial and complex claims about the ability of languages to contain semantic apparatus applying to themselves.
- That should have been fixed 5 years ago, but it is done now. As for the other comment above this, I don't think it can be done. It's an issue of metalanguage. I've removed unsourced parts of the article which claimed otherwise per WP:REDFLAG and WP:OR. Tijfo098 (talk) 10:54, 30 March 2011 (UTC)
Problems
I think there are problems with the laws of logic in this article. For example:
The statement "This statement is true" is both true and false. The statement "This statement is false" is neither true nor false. —Preceding unsigned comment added by 144.173.6.67 (talk • contribs) 16:20, 18 October 2006
Vagueness
I've done much fixing of the article, but the vagueness section is still much in need of repair. — Charles Stewart (talk) 19:58, 30 June 2009 (UTC)
Some issues with semantics of bivalence & gappiness
From my recent revert:
- There is no n-ary generalisation of bivalence worth noting. Bivalence is not about truth tables, it is about truth. To apply bivalence to a many-valued logic, one identifies some set of propositional values as true, and the others as not true.
- "Gap theory" means Gap creationism (20 000 ghits vs 46). I don't think it can be right to talk of a particular theory or family of theories identified only by rejection of bivalence. But the content here is worth rescuing:
A theory that rejects bivalence is sometimes called `a gap theory'. Gap theories allow that some sentences may lack a truth value, or that there are more than two semantic values. Some motivations for rejecting bivalence are: * Intuitionism: If truth is grounded in verification or proof conditions, then since some sentences are undecidable or undecided they are neither true (provable) nor false (refutable). * Irreferential (non-denoting) singular terms: If a sentence involves an irreferential singular term like 'Pegasus', it is truth-valueless ("gappy"); * Future contingents (see next section); * Paradoxes: E.g. Kripke's theory of truth deems the liar sentence gappy; * Vagueness (see below).
- The discussion in "Bivalance and non-contradiction" seems useful to me. I don't see why nearly all of it should be deleted.
The point about Boolean subalgebras is a good one. It may be worth having a section on algebraic semantics that explains why Stone duality has led some to reject bivalence. — Charles Stewart (talk) 08:06, 3 July 2009 (UTC)
Bivalent logic
Bivalent logic redirects here - what does it mean? Is it correct to say bivalent logic describes the set of logic systems that have only two values, and binary logic would be an exemplary member of this set? Are bivalent logic and two-valued logic synonymous? --Abdull (talk) 21:55, 8 February 2010 (UTC)
- Yes, bivalent and two-valued are synonymous. Binary is also a synonym, but "binary logic" is usually used in digital circuit engineering, so it usually means propositional two-value logic. Perhaps that one should be redirected elsewhere, like to logic gate. Tijfo098 (talk) 10:12, 28 March 2011 (UTC)
- I have made binary logic a dab. Tijfo098 (talk) 10:50, 28 March 2011 (UTC)
Rename request
{{Requested move/dated|Two-valued logic}}
Principle of bivalence → Two-valued logic — Occurs twice as often in google books compared to the current title. Tijfo098 (talk) 06:32, 28 March 2011 (UTC)
- Comment what about "binary logic"? 65.93.12.101 (talk) 06:36, 30 March 2011 (UTC)
- That is too ambiguous, see section above, and the binary logic page itself. Tijfo098 (talk) 09:30, 30 March 2011 (UTC)
I don't doubt that the term "two valued logic" appears more, but I think "principle of bivalence" is a better title for an article that deals with the philosophical aspects. The issues with formal logic are a secondary issue for this article; the real meat is the philosophical issues, such as whether a hypothetical event in the future must have a determinate truth value in the present. Doing a search on Google books is going to catch a lot of sentences like "this is a two valued logic" that are not very relevant to this article. — Carl (CBM · talk) 10:34, 30 March 2011 (UTC)
- You're right, my proposal would inadvertently narrow the scope of the article to the more technical issues. So I'm withdrawing the move request. Tijfo098 (talk) 10:46, 30 March 2011 (UTC)
New request
Principle of bivalence → Bivalence — There are quite a few Google books hits which talk of this topic without "principle of" or using "law of" instead etc. So it seems more natural unprefixed. (Compare with extensionality, which also has "principle of" appearances). Tijfo098 (talk) 11:06, 30 March 2011 (UTC)
Confused about Boolean valued logics vs. classical logic
Takeuti says that any complete Boolean algebra is a good model (presumably as in model theory) for classical logic.
Bell et al. on the other hand say that "Boolean valued logic is classical logic", but they seem to refer to only propositional calculus and any Boolean algebra via Lindenbaum–Tarski algebra.
I'm missing something here; why is Bell not talking about complete Boolean algebras? I suspect they mean different things by "classical logic", perhaps propositional vs. ??? Or perhaps Bell is assuming the "Boolean valued logic" being over a finite Boolean algebra (which is complete)? Tijfo098 (talk) 09:44, 28 March 2011 (UTC)
- I don't have the full context of those excerpts, but I think Bell is referring to these theorems:
- A sentence S is provable in classical propositional logic if and only if, for every Boolean algebra and every assignment of the letters of S to elements of the algebra, the corresponding value of S is the maximum element 1 of the algebra.
- A sentence S is provable in intuitionistic propositional logic if and only if, for every Heyting algebra and every assignment of the letters of S to elements of the algebra, the corresponding value of S is the maximum element 1 of the algebra.
- No completeness is needed in the algebra. Takeuti is also referring to the theorem of the first bullet there, I believe. — Carl (CBM · talk) 13:58, 28 March 2011 (UTC)
Actually, no, they are not talking about the same thing! You can give boolean valuations to predicate logic. This requires inf for ∀ and sup for ∃. That's why you need a complete Boolean algebra in general for classical predicate calculus. See [1] and verso. I'm in hurry now, so I'll fix the article later... Tijfo098 (talk) 18:48, 29 March 2011 (UTC)
- For predicate logic, you can use complete Boolean algebras, but you can also use cylindric algebras, which is how people who want to do algebraic logic seem to do it. I'm not very familiar with cylindric algebras, though. The theorem I wrote above was intentionally stated just for propositional logic, where completeness is not needed. — Carl (CBM · talk) 18:57, 29 March 2011 (UTC)
Extensionality / Compositionality
This edit removed the text on that, claiming the source doesn't talk about it, but note that extensionality is given in italics in the source, and if you google around, there are other sources talking about it as "principle of extensionality" in the same context. [2] [3] etc. In other words, engage the google before you press the delete button. (And there is such non-trivial thing as axiom of extensionality which expresses that in ZF.) Tijfo098 (talk) 12:37, 29 March 2011 (UTC)
- The axiom of extensionality in ZF is quite different: it says that two sets are equal if they have the same elements. The "principle of extensionality" is usually described by just saying that classical logic is "truth functional" - that the truth values of a compound sentence depend only on the truth values of the parts. But, it is possible to use truth-functional logics that study set theory without the axiom of extensionality (this is actually common in type theory, less so in set theory). So the principles are not the same, although they are both about some distinction between extensional and intensional systems.
- I also was unsure whether the extensionality remark was appropriate for this article. But really that whole paragraph is a little unclear (the "characterized" claim justifiably has a "vague" tag on it), so I thought I wouldn't change it unless I rewrote the whole paragraph. — Carl (CBM · talk) 12:54, 29 March 2011 (UTC)
- I did rewrite the paragraph a little while ago, what do you think? — Carl (CBM · talk) 13:39, 29 March 2011 (UTC)
- To Tijfo098: If you had given pointers to [4] and [5], I would have known what you was referring to. Nevertheless, there are two issues. First, this notion of "extensionality" is not very common, and compositionality is indeed most common in this context. Extensionality usually means that pointwise (or element-wise in set theory, or observational in computer science) equality implies equality (try "principle of extensionality" in google, even though the most common name is axiom of extensionality). Secondly, compositionality is a property shared by many logics, so I don't think it is relevant to put a focus on it specially for the case of classical logic. But maybe, I missed the point? --Hugo Herbelin (talk) 14:15, 29 March 2011 (UTC)
- (edit conflict) Thanks. I've linked extensionality as "see also" instead (that article does talk of the axiom of extensionality however). On the other issue (of Boolean-valued semantics/models), isn't the "Algebraic semantics" section now redundant to what you wrote? (Before you moved & rewrote it that paragraph was in the lead). Tijfo098 (talk) 14:20, 29 March 2011 (UTC)
- One more point: Some people refers to the principle (p ↔ q) → (p = q) as propositional extensionality (see e.g. [6]) but it is still different from what the references you are giving say (afaiu, what they express is the property that the value of φ(p) when p is an arbitrary formula is the same as the value of φ(x) when x is an atom whose value is given to be the one of p). --Hugo Herbelin (talk) 14:34, 29 March 2011 (UTC)
- That is more of the type of extensionality that people study in type theory or set theory. If you replace the "propositions" in that link with sets, what you get is exactly the set theoretic axiom of extensionality. — Carl (CBM · talk) 14:41, 29 March 2011 (UTC)
- (edit conflict) Thanks. I've linked extensionality as "see also" instead (that article does talk of the axiom of extensionality however). On the other issue (of Boolean-valued semantics/models), isn't the "Algebraic semantics" section now redundant to what you wrote? (Before you moved & rewrote it that paragraph was in the lead). Tijfo098 (talk) 14:20, 29 March 2011 (UTC)
- I don't really understand what the second paragraph of the "Algebraic semantics" section is trying to say. So I guess I wouldn't mind removing it, unless someone else can rephrase it to bring out the main point. I agree it's somewhat redundant to the text I wrote this morning.
- The link to Boolean-valued model is not so great because that article focuses mostly on models of set theory. That's why I left a red link to Boolean-valued semantics in my text. It would take me a lot of work to write a decent article on that, because I would have to read up on algebraic semantics and because I don't know of good references for things like the two theorems I wrote higher on this talk page. So I just made a link for now. — Carl (CBM · talk) 14:27, 29 March 2011 (UTC)
Hmm, if you guys are right, then Extensionality should be split in two articles. But I don't think you are! In PL terms extensionality is deep equality, and intensionality is shallow equality [7]. Tijfo098 (talk) 15:24, 29 March 2011 (UTC)
- I'm just saying that "extensionality" in type theory or set theory is not the same as "extensionality" of truth values. In type theory, extensionality of a functional means that it gives the same results on extensionally equal inputs. In these philosophical books, "extensionality" of a logic means that if subformulas of a formula are replaced with equivalent subformulas, the overall formula has the same truth value. But subformulas are not "inputs" to the larger formulas. For example the subformulas themselves may have subformulas, which are still subformulas of the original formula, and just those sub-subformulas could be substituted instead. That has no analogue in substituting arguments of a functional in type theory. — Carl (CBM · talk) 11:02, 30 March 2011 (UTC)
- "But subformulas are not "inputs" to the larger formulas." Aren't they? What about functional PLs like Haskell, where "subprograms" are exactly subformulas (Haskel programs are executed by expanding a graph of formulas with subformulas until one reaches the terminal nodes), and in general the Curry-Howard isomorphism. I think it depends what "are" means in your statement. I think [8] hits the nail here: "These principles [bivalence & exntensionality] form only an idealization of the actual relationships." Tijfo098 (talk) 11:58, 30 March 2011 (UTC)
- No, I think they are not. In a formula like , there are no "inputs" whatsoever (no free variables). The subformula R(x,y) is not an "input" in any sense; R is not a free variable that can be replaced. And even if it was able to be replaced somehow, the entire subformula would also be an "input" subject to replacement. But then it is no longer possible to change one "input" independently of changing another "input". So it's true that classical logic is truth functional, but the sense in which this is a form of extensionality isn't the same as the sense in which equality of sets is extensional. — Carl (CBM · talk) 13:16, 30 March 2011 (UTC)
- "But subformulas are not "inputs" to the larger formulas." Aren't they? What about functional PLs like Haskell, where "subprograms" are exactly subformulas (Haskel programs are executed by expanding a graph of formulas with subformulas until one reaches the terminal nodes), and in general the Curry-Howard isomorphism. I think it depends what "are" means in your statement. I think [8] hits the nail here: "These principles [bivalence & exntensionality] form only an idealization of the actual relationships." Tijfo098 (talk) 11:58, 30 March 2011 (UTC)
I managed to find sources that call the extensionality of equality the replacement property [9] [10]. I think this terminology makes more sense in the context of syntactic replacements, which is what we are discussing here. See also Kleene (gives both terms) and footnote 92 defines extension of a predicate by means of a set. Tijfo098 (talk) 14:37, 30 March 2011 (UTC)
- Fitting and Kleene are indeed talking about extensionality of equality, not about replacing arbitrary subformulas. That's not the same as replacing subformulas, though.
- Gibbay et al. state a weak form of replacement for subformulas on p. 124, but they don't state a general principle that when two formulas are logically equivalent (that is, their universal closures are equivalent) then one can always be substituted for the other in a larger formula. — Carl (CBM · talk) 16:01, 30 March 2011 (UTC)
- Well, p. 124 is for FOL. But it seems you missed page 8, [11] which is where they formalize their statement from the introduction as Lemma 1.1.3, which is about certain kinds of propositional calculus (not necessarily classic, but including it). Tijfo098 (talk) 16:32, 30 March 2011 (UTC)
- I can't see that page. Frankly, it's very difficult to tell what your argument is when it relies on me having to guess what you see in links to google books. Could you just come out and say what you mean, so that it isn't necessary for me to follow links? That would make the conversation much more efficient, and I would appreciate it. — Carl (CBM · talk) 16:37, 30 March 2011 (UTC)
- Well, p. 124 is for FOL. But it seems you missed page 8, [11] which is where they formalize their statement from the introduction as Lemma 1.1.3, which is about certain kinds of propositional calculus (not necessarily classic, but including it). Tijfo098 (talk) 16:32, 30 March 2011 (UTC)
Frankly, I'm not quite sure what exactly is your point either. I have been assuming you are objecting to calling "replacement for subformulas" (the principle of) extensionality. This is a terminology issue. I think I've shown above that there are sources calling it that way, and there also sources calling it "replacement rule/principle" as well (which seems more natural to me). You appear to me to think to think otherwise, and say no such rule/principle is mentioned anywhere in those sources, i.e. that I'm misinterpeting all of them. It's not really an important issue with respect to this article, so let's just end this futile conversation. Tijfo098 (talk) 17:50, 30 March 2011 (UTC)
Whole article is based on a false premise
There have been so many comments on this page in the past seven days that I thought I would just start a separate section rather than try to answer them individually.
The article starts out by defining the principle in question to be that "every declarative sentence expressing a proposition (of a theory under inspection) has exactly one truth value, either true or false.[1]"
It then goes on to say that "A logic satisfying this principle is called a two-valued logic[2] or bivalent logic.[3]"
Now the problem with this is that Boolean algebras are traditionally distinguished from Heyting algebras as being the algebra of two-valued logic. This is not the same thing as the "principle of bivalence" if we are to believe the article's definition of the concept. Picture a universe consisting of two places, Paris and London, each with two states, raining (1) or not raining (0). Then the proposition "it is raining" has four truth values, namely 00, 01, 10, and 11, because it can be interpreted in either Paris or London, and for each such interpretation the proposition further has two interpretations, that it is raining or not.
Nevertheless this proposition is interpretable in a two-valued logic, because there is no question that "either it is raining or it is not raining" (unless you want to quibble over drizzling or snowing). Regardless of whether we are interpreting this proposition in Paris or London (for definiteness, the centre of each say), one or the other possibility must be the case.
Until the article comes to grips with this issue it must be considered confused. Attempts to fix it are equally confused as long as they don't come to grips with it either.
The interesting question for Wikipedia is where it wants to position this article. If as a contribution to fuzzy thinking (and Wikipedia is full of such articles, for example the one on the greenhouse effect) then it is an ideal, even exemplary, candidate. If as a contribution to what Ernst Schröder called "exakte Logik" however then the sooner it is deleted the better, as there is no obvious logic article to redirect it to. --Vaughan Pratt (talk)