3 ms·
Actually, it's a very simple practical counterexample to the "law of excluded middle" logic axiom. [1] The situation described in the puzzle did physically exi
by TuringTest 11y ago
Actually, it's a very simple practical counterexample to the "law of excluded middle" logic axiom. [1]
The situation described in the puzzle did physically exist when the photo was taken, yet the truth value of the first label is neither true nor false. It that's a troll, then trolls like this provide food for thought.
[1] https://en.wikipedia.org/wiki/Law_of_excluded_middle https://en.wikipedia.org/wiki/Law_of_excluded_middle
- JadeNB 11y agoI think that this is not the correct interpretation of the law of the excluded middle. It says that `P or not-P`; that is, that P is true or not-P is true. That's different to saying that P is true or P is false; confusing "not-P is true" with "P is false" is exactly the distinction that logics, such as constructive logic, that avoid LEM try to avoid. (At least for me, it helps to think in terms of proveability, not of truth, which is, I think, almost what constructive logic does; there is a difference between saying that "P is not proveable" and "not-P is proveable".)
- TuringTest 11y agoI keep telling myself that I should learn more about constructive logic, as my own intuitions tend to it. I get that in such logic you can't deduce "P is false" directly from "Not-P is true", and you have to build an explicit derivation for the former?
- JadeNB 11y ago> I get that in such logic you can't deduce "P is false" directly from "Not-P is true" It's actually the other way around; if not-P is true, then P is false, but not conversely. (The computer-flavoured example that comes to mind is that it is not possible to decide equality of functions (so `P or not-P` fails), but any two functions either are (`P` is true) or are not (`P` is false) equal. Again, this confusion between truth and decideability is, I think, not quite rigorous, but it gets at the essential idea.) > I keep telling myself that I should learn more about constructive logic, as my own intuitions tend to it. Indeed, Brouwer's precursor of constructive logic was called "intuitionistic logic" precisely because he felt that it better captured an intuitive, rather than formalist, approach to reasoning. (I'm not sure I agree ….)
- TuringTest 11y agoFor me, the important intuition in this regard is that, for any mathematical theory to be useful, you need to create a process where you can prove properties about its objects in a finite number of steps. You can handle infinite objects (like sets), but at some point you need to define a finite process that produces some knowledge about the object (for example, deciding if a particular word is a member of an infinite grammar). Working with infinite objects is like using lazy computations in a functional language - you only use as many steps as needed, even if the process does not have a termination step. (I'm not sure to what degree constructive logics handle this intuition - as I said, I don't know much about them). I've seen that some models exist for mathematical proofs containing infinite steps, but those don't seem to be widespread - and the models are themselves defined through a finite description; so I think even this extreme case validates my intuition that in the end, the mathematician needs to include just a limited number of clauses in their day-to-day work to get something done, even if those clauses are used to describe infinite objects.