Logic

This room is meant for discussion about logic, including foundations, deductive systems, proof theory, computability theory, model theory, ...
5h ago – Jade Vanadium
Jade Vanadium: 5h ago, 3180 posts (4%)
217

export all events for this room

Starred posts

1 2
Feb 25, 2024 10:00
Very good question. There are a bunch of different uses, but basically it's used as a tool to measure how susceptible an ordinal is to Replacement. So, the basic idea is, consider an ordinal number β (or it can be a wellordered set, or whatever). Given a subset S⊆β, we say that S is cofinal in β when: for all x<β, there exists y∈S such that x≤y. Since β is wellordered, then S is also wellordered, hence S can be assigned an ordinal number order type...
Nov 23, 2020 07:23
The reason is simple. One cannot study logic without using logic, and if one is unfamiliar with formal logic then it is almost impossible to be clear about what is going on. Indeed, before FOL you of course need to learn PL (propositional logic), and after FOL you still need to learn to use it in actual mathematics, for which I always suggest PA (Peano Arithmetic). It will only take a few weeks for you to learn all that, if you set your mind to it!
6
Nov 14, 2017 11:25
I love teaching logic hahaha..
10
Oct 18, 2017 15:09
=== Godel/Rosser's incompleteness theorem and simple computability proofs ===

Here I shall present very simple computability-based proofs of Godel/Rosser's incompleteness theorem, which require only basic knowledge about programs. Both proofs are by contradiction, and hence do not give an explicit independent (neither provable nor disprovable) sentence. In contrast, there are proofs that give an explicit independent sentence by using essentially a fixed-point combinator applied to provability, but that are quite a bit harder to understand than the unsolvability of the halting problem. It s
6
Jul 27, 2018 04:21
I suppose I'm in the logic room now
5
Sep 3, 2020 13:16
So you know why I use "⇒" all the time for implication! =D
2
Dec 9, 2017 05:07
be logical
4
Oct 15, 2017 17:32
I will hold a discussion type of class on sunday UTC 11am−1pm on Godel/Rosser's incompleteness theorem and simple computability proofs. All are welcome to join, but please read through the pinned post before attending!
4
Dec 5, 2021 10:36
Incidentally, there are harder types of 'quines', such as a program that prints the SHA256 hash of its own source code. I can never remember how to do that. Maybe I should try again for fun haha..
Aug 2, 2017 20:07
@user21820 what I don't understand is some mathematician's attitudes of trying to prove induction
3
Jun 5, 2021 06:16
0
A: Must a sequence be a function on $\mathbb{N}$?

user21820As Xander says, mathematical definitions are not things to be proven. However, I disagree with some points in his post, not because it contains wrong mathematics but because there is a better way from a logic-based viewpoint. The whole point of the notion of "sequence" is to capture some kind of ...

Mar 12, 2017 01:54
It is indeed usually inactive, I think because too few people understand their severe lack of logic is impeding their grasp of mathematics. Even teachers in my educational institution do not appreciate the problem.
3
Dec 25, 2018 08:13
Happy holidays to you both! =)
2
Aug 29, 2016 15:59
Haha! I recommend you don't bother with Philosophy SE, because almost all of them (except perhaps Cort Ammon and Mauro Allegranza) do not know enough logic to be able to give a correct answer for deeper questions!
3
Aug 18, 2016 07:21
@MartinSleziak: And what to do with crankpots who keep posting nonsense about Godel's incompleteness theorem? I'm tired of them already.
3
Nov 22, 2020 19:35
Just to demonstrate, I will give a rigorous 1-page proof of the fixed-point lemma relying on basic FOL and the representability theorem and nothing else.
Sep 28, 2020 04:21
And yes I recommend Rautenberg's "A Concise Introduction to Mathematical Logic". It really lives up to its name for conciseness; it packs a lot in a single book! =)
Jan 4, 2018 05:42
2
Q: Computable extension to $Σ_1$-sound system that is $Σ_2$-unsound?

user21820Recently, I wrote this post showing (if I did not make a mistake) essentially that: For any nice formal system $S$ that is $Σ_1$-sound there exists some extension $S'$ that is $Σ_1$-sound but $Σ_2$-unsound. (Here "nice" is the usual kind of technical requirement, but you could simply assume t...

2
Dec 19, 2017 05:45
@user21820 If I understood correctly, the outcome of this theorem is we can show every tautology is a theorem, and that the proof of this theorem is possible because our formal system has sentence of finite length consists of finite number of boolean operators thus allowing us to do structural induction on it?
2
Sep 16, 2017 11:52
there's little i know, more that I don't know, and even more that I don't know that I don't know
2
Jun 12, 2020 11:43
It also shows clearly that his putting "sets" at the bottom is misleading or outright wrong. Within the foundational system of ZFC, of course sets are not axiomatized because they are already governed by the foundational system and need no further characterization. Hence a lot of mathematicians outside set theory view sets as structureless. But clearly ZFC sets viewed from a different foundational system would be rather complex!
Jul 17, 2017 20:17
@user21820 "I fear that in today's foundation-free mathematical education students just accept accept everything that is offered, rapidly training themselves in showing the behavoir that is expected from them." Not all of us are mindless sheep! :D
2
Jun 13, 2017 11:30
It's possibly the most neglected field in education today.
2
Apr 11, 2020 20:30
shakes fist at authors who are the only people who understand their work
May 28, 2017 19:39
@user21820 Hello! I miss seeing you in the "Realm". I hope all is well,
2
Apr 29, 2017 09:00
That said, I won't worry about people stealing your ideas. Nobody wants to steal ideas about logic.
2
Aug 12, 2019 14:59
@Slereah If you're talking about a formal proof, depends on which style of deductive system. I think the only style that is humanly usable for actual mathematics is Fitch-style or something like it.
Nov 11, 2018 04:44
Game semantics can avoid assuming a completed infinity or even a potential infinity, as it can be restricted to the limit of physical capability. The notion of consistency also splits, in the sense that it is possible for PA to have no classical model but yet be consistent since "there is no proof of 0=1 that is 'short enough' for anyone to write down and verify".
Nov 4, 2018 17:29
Set Theory: Boolean-Valued Models and Independence Proofs.
Oct 28, 2018 17:44
Incidentally, this is one of my pet peeves from people I know who sort of know about physics: the idea that superposition is "and".
Mar 24, 2018 13:16
Induction: For any property P of naturals, "P(n)" denotes "n satisfies P", and we have ( P(0) ∧ ∀n∈N ( P(n) ⇒ P(n+1) ) ⇒ ∀n∈N ( P(n) ) ).
Mar 9, 2018 10:11
@WhatsThePoint It's okay. Just ask about anything that is unclear to you or that you want to know. Aim for 100% understanding, and you'll get there!
Mar 2, 2018 08:38
In summary: (1) It is wrong that ~ defined via the axiom "forall x,y ( x~y iff forall z ( z in x iff z in y ) )" satisfies substitution. (2) One has to add an extra indistinguishability axiom (my own name) "forall x,y ( x~y implies forall z ( x in z implies y in z ) )" because it cannot be proven otherwise and yet is an instance of substitution. (3) Once you have added the indistinguishability axiom, ~ will satisfy substitution.
Feb 17, 2018 05:41
See plato.stanford.edu/entries/self-reference and search for "Kleene", but don't go to the linked article on many-valued logic, since Kleene's 3-valued logic is already defined there.
Feb 17, 2018 05:34
> Sometimes if you ask whether an object is a real, you will get no answer.
Feb 3, 2018 06:33
Note that the typical geometric proof is arguably pedagogically defective because it relies on geometric notions which are quite impossible to make rigorous without analytic euclidean geometry. In any case, if one really wants to invoke geometry, the easiest way is to use rotation matrices.
Jan 27, 2018 04:29
@LeakyNun: Um before you go away with the wrong impression, you can't just modify PA the way I stated. You have to add some reflection axioms as well and some other stuff before you get the system that proves its own consistency.
Jan 27, 2018 04:08
@LeakyNun: Hey I found this recent arxiv article from Dan Willard, but haven't read it. The reason I searched for this guy is that he created a system that is similar to PA but with addition and multiplication replaced by subtraction and division, and that proves its own consistency. So I was wondering whether his system proves the counterpart of Fermat's little theorem. Not sure whether the article I found does that, since this theorem is Π1.
Jan 12, 2018 03:43
@DavidReed That's a popular phrasing, but it's arguably wrong and misleading. What it truly means is to make the weakest collection of assumptions that suffices to explain what you want to explain, not necessarily the fewest.
Jan 4, 2018 05:41
1
A: Can there be two different math?

user21820Yes. Let $S$ be our chosen foundational system. Even if we somehow know that $S$ is $Σ_1$-sound, we still cannot rule out the possibility that $S$ is $Σ_2$-unsound! Here truth and arithmetical soundness are of course defined with respect to the natural numbers in the meta-system. First conside...

Dec 17, 2017 06:41
You could think of it as modal necessity of the reason implying necessity of the result.
123
Nov 14, 2017 11:25
I can see that.
Nov 3, 2017 17:11
@GabrieleScarlatti Hello! You could think of it that way. But at least from my point of view I don't consider it 'vacuous'. It makes more sense to call "∀x∈S ( P(x) )" vacuously true if S is empty, because P does not matter. But in your case when "P ⇔ Q" is true, it does matter what both P,Q are; if one is false you must have the other false too.
Nov 3, 2017 17:11
It's not assume true, by the way; it's defined to be true when the two subexpressions are either both true or both false.
Oct 26, 2017 09:58
Otherwise condition (2) suffices. Namely, if you can show that ( given any object x in S, if every object in S of smaller size than x satisfies P, then x itself satisfies P ), then every object in S satisfies P. Size is captured above by f.
Oct 26, 2017 09:55
It applies whenever you have a collection S and a function f : S → N, and a predicate P : S → bool. Then structural induction says: ∀x∈S ( ∀y∈S ( f(y)<f(x) ⇒ P(y) ) ⇒ P(x) ) ⇒ ∀x∈S ( P(x) ).
1 2