And I just read again your argument why PA is so important, which seems to contradict my point that it is simply an application. I am sure that you know what I mean when I say it is an application of logic. It's me that did not show that I understand what you mean by PA being so important. I think I do understand it.
I think it's just one of those things where the same concept shows up at different levels, just like set theory can be under the semantic and can also be an application of logic. So, I think that the occurrence of PA that you find so important is not at the level the formal semantic. It is at a different level, which is part of the deductive system side.
Ok, I have read again what you said about robust and strong and I could not make sense of it with the definition of semantic that I have. Moreover, I could see that your notion of semantic is more on the deductive system side and it explain why PA is so important in your view of semantic. So, we were not talking the same language.
In my view, which I believe is Manzano's view, we differentiate semantics in terms of the structures considered: if we consider free structures (frames), then it's one semantic. If we consider the Henkin (or general) structures, then it's another semantic. If we consider full (or standard) structures, then it's yet another semantic.
Your view of semantic is more like the semantic of a program in computer science. This is a different concept, more on the side of the deductive system, which you identify with a theorem prover. BTW, I have no problem in identifying a deductive system with a theorem prover, because the important aspect is indeed the sentences that can be proven.
However, I think the concept of logic is way more than the concept of a theorem prover and thus way more than a deductive system, in this general sense. I know you agree, because you have two additional criteria: strong and robust. However, you use a completely different notion of semantic to express these criteria.
I disagree that they are the same as mine: (1) definability of the structures and (2) the class of structures must be as large as possible, with (1) having priority.
You might be right that these criteria do not extend to intuitionistic logic, etc. So, it might fail as a general approach, but if you judge whether it can go beyond HOL based on your notion of semantic, it means nothing.
And now I have read that you agree that we can useful stuff that are incompatible. So, the main issue is that we used a different notion of semantic. We were not talking the same language. It's important, because we therefore have different ways to determine what is an "interesting" logic. It could be that yours is more general, but it does not match with the beautiful criteria discussed by Manzano.
@Dominic108 Yes, my notions are more general, but of course greater generality means we would get less about any specific class of formal systems. This trade-off is unavoidable. And yes, there are very nice results for FOL (and HOL with Henkin semantics), and that is why it is important that so far every formal system with practical applications can be translated quite naturally into HOL. There is no need for us to go beyond HOL unless we want to articulate what "natural" here means.
@Dominic108 I didn't say there is a problem with intuitionistic logic at all. I suggest you quote me whenever responding, because it's likely you have misread a number of my statements.
This isn't bad per se, it's just that it's not so simple as "weaker implies better".
The reason I mention incompatible extensions of a weak system is that different people have different notions of what 'true mathematics' can be. Just for example, Brouwer proved that every function from R to R (where R is the reals) is continuous! Do you buy that? Do you think it really is useful? Why or why not? Note that Brouwer was indeed working within an intuitionistic system extended by some axiom that allows the deduction of such results.
In my opinion, there isn't a right or wrong answer to my above question, because it's about reals, which are in the first place a conceptual (and not really real-world) notion. So it would come down to our personal philosophy of mathematics.
@Dominic108 But in my opinion, all practical foundational systems must interpret classical PA or at least something very close to it, because without that we cannot reason about finite program runs. Our creation of computers and various algorithms relying on PA have also created a vast amount of empirical evidence for the soundness of PA up to at least 2^1024. Furthermore, one cannot even reason about FOL without relying on a classical theory of finite strings!
More specifically, to even prove that every FOL theory is either consistent or inconsistent requires LEM for Σ1-sentences. So to me it doesn't make sense to consider the possibility that Σ1-LEM fails. But as per the linked posts about 3-valued set theory and paradoxes, I think LEM is not quite justified for general non-arithmetical statements, and so one can indeed consider 3-valued or intuitionistic foundations and see whether one likes what it proves.
Given my understanding of what you mean by semantic I don't disagree with what you say. It has not much to do with my view of semantic, which is also a view implicit in Manzano's book. She does not formally define semantic, but she clearly separate semantics in terms of the class of structures. It is this way to distinguish semantics that I consider.
Oups, I had not read all your replies, only the last one. I did not realize it was possib
Oups, I had not read your entire reply.
I use my mobile and I posted early by mistake. I realize now that it was a single reply in many parts. The key point is that I had only read the last part.
Ok, I have now read your entire reply. What can I say. You seem not to realize at all that you discuss something different. It seems that we agree on most conclusions. For example, we agree that contradiction between applications of logics (this is my way of saying it) are not bad.
However, in my view, contradiction between logics would be bad. But, I see that with your definition of deductive systems contradictions between them are not bad and, I agree, because ...
... in my view your are talking about applications of logics. All of this because you do not consider my view on semantic and the associated criteria. Again your notion of semantic is entirely on the deductive system side, not mine.
@Dominic108 I know that you are concerned with semantics as defined in Manzano's book. I already said that if you do so then you are arbitrarily restricting yourself to FOL or FOL-like logics, which is not a problem, just that you cannot compare these with other logics that don't fit into the nice box. That's all.
But it is not true that your view of semantic is a generalization. It cannot be the case, because it is about truth on the deductive system side. Manzano's semantic brings a second notion of truth. You don't generalize that.
It's not a generalization. You speak a different language.
@Dominic108 Your comment makes no sense to me. I never once said that semantics is solely about natural numbers or strings alone. As I said before, if you don't quote me explicitly, please don't put words into my mouth. It is not courteous and does not contribute to the discussion.
I never said that you said that. I say that your notion of semantic is entirely on the deductive system side, not on the side of any specific deductive system. By this I mean that you use it to define truth on that side.
@Dominic108 Your last comment still makes no sense to me. I never implied anything of that sort. If you don't want to quote me, don't say that my notions are like this or like that, when they are not.
Yes it makes no sense to you. This is consistent with what I am telling you. You speak a different language not consistent with Manzano ways to classify semantics.
@Dominic108 I know that you are concerned with semantics as defined in Manzano's book. I already said that if you do so then you are arbitrarily restricting yourself to FOL or FOL-like logics, which is not a problem, just that you cannot compare these with other logics that don't fit into the nice box. That's all.
I am also using "semantics" in the original sense of the word (and in the sense that logicians I talk to use it), not in Manzano's idiosyncratic sense.
Ok, but earlier you said that your approach was a generalization. This was my concern. Also, I see nothing in what you wrote that explain why Manzano's view cannot be generalized. I am not convinced.
There is a subtle issue here. Manzano's has not defined semantics as a class of structures. I was wrong about that. But she clearly focuses on classes of structures, free structures, standard structures, Henkin structures, etc and distinguish semantics using these classes.
@Dominic108 Right. So? If you read widely enough, you will find that the general use of the word "semantics" in the logician community is a vague notion, and necessarily so, for the same reason that I say that HOL is a nice but restrictive box.
Now, there is a separate notion of truth associated with a class of structures. It is only the same in the special case where the deductive system is complete and sound.
Yes, and normally when people devise a new logic system they will have to come up with some kind of semantics for it. The semantics devised for classical logic is clear-cut and nice. But it's ad-hoc for every logic.
Even Kripke semantics came about half a century after intuitionistic logic.
In any case, I don't mean "a way to fix what is true on the deductive system side". I mean exactly what the English word "semantics" means, namely to assign meaning to syntax. This may not have anything to do with deductive systems.
So I did not assume anything about Kripke. Maybe. I can see a sign that you have written something new, but I have already written my text...
This notion "attach meaning to syntax" is very general. The classes of structures don't do that in themselves. It is only when we use them for interpretation and require soundness and completeness that they play a role in that sense.
Yes, but when you say that PA is very important for this semantic, it does not match with Manzano's way in the following sense that it has not much to do with classes of structures.
And I want to emphasize what you just said: The class of structures don't in themselves attach meaning to first-order syntax. You need to view it from an external (even human) viewpoint. And logicians in general use "semantics" to mean "meaning", so you can maybe now see why I use the word the way I did.
@Dominic108 I didn't say PA is very important for semantics.
Since you don't want to quote me, I'll quote myself. =)
@Dominic108 But in my opinion, all practical foundational systems must interpret classical PA or at least something very close to it, because without that we cannot reason about finite program runs. Our creation of computers and various algorithms relying on PA have also created a vast amount of empirical evidence for the soundness of PA up to at least 2^1024. Furthermore, one cannot even reason about FOL without relying on a classical theory of finite strings!
Note the words "practical foundational systems".
And "interpret" here is a technical term. You should have asked if you didn't know what I meant.
I asked you a question (which you haven't answered), and explained that I didn't think there was a right/wrong answer to that. I then commented that I do think that there is a right/wrong answer to whether practical foundational systems should interpret classical PA or not.
@Dominic108 That's a separate question. I think it's obvious once you learn enough about intuitionistic logic, Kripke frames, and type theories.
I don't have any problem about the fact that we can prove different things when using different premises. I don't see the link with classes of structures.
First-order structures are tied to first-order languages. Second-order structures are tied to second-order languages. Even the form of the signatures are tied down. Obviously, for formal systems that simply aren't based on the same kind of languages, you will need to devise 'structures' that are idiosyncratic to those kind of systems. Clearly then, there is no single notion of "structure", much less "class of structures", for general logics or formal systems.
Basically, the answer to "why we cannot use this concept of classes of structures in general" is "the existing notions of 'structure' is not general enough unless you stick to something like HOL".
I had done it for "this is a separate question". I guess I meant separate from what? Were you saying that the question of classes of structures is separate.
Anyway, do you know a deductive system for intuitionistic FOL, and how it differs from a system for classical FOL? And do you understand Kripke frames?
What is separate from this? Anyway, I am sure that separate things have been said. Don't assume that I confuse them. Perhaps I simply see that they are not linked to classes of structures and this is my focus.
No I said many times that I need to study these things. It may be difficult to show why classes of structures do not apply
@Dominic108 Okay enough of going on and on about my use of "separated". Other native English speakers can see that you had misunderstood me from the beginning. Let's just stick to the mathematics. I want you to first study a deductive system for intuitionistic FOL, and then try on your own to come up with 'structures' that can be used to assign meaning to intuitionistic FOL. Without trying, you're not going to understand.
After your attempt succeeds or fails, you can learn about Kripke frames, which fulfill that purpose. After that, then perhaps our discussion will be more fruitful.
You do claim that the way Manzano uses classes if structures (which is most likely the way they are used in general for HOL) cannot be generalized to intuitionistic logic and other logics.
@Dominic108 I claim that any such generalization is necessarily ad-hoc. And my evidence is that Kripke frames were applied to intuitionistic logic only half a century after the deductive system itself had been devised.
I don't know what you mean by a generalization that is ad-hoc. I suspect hat the generalization will not come with a proof that nothing can be more general. But if it includes Intuitionistic + HOL then it's interesting.
Let's use a mathematical analogy. Extending classical FOL structures to Kripke frames is like extending natural number exponentiation to real number exponentiation. Asking to extend further to arbitrary 'logics' is like asking to extend exponentiation to all kinds of 'numbers' that will be invented, like ordinals, cardinals. Sure, people have indeed done so, but those exponentiation operations are as different as birds and fishes.
In HOL you have higher-order sorts, and like SOL you need to specify the signature of each non-logical symbol in terms of the input sorts, so any 'structure' for HOL must also interpret these in a manner consistent with the intended meaning of the higher-order sorts... For example, if f is of sort S→T and x is of sort S, then f(x) in a HOL structure must be of sort T. This is peculiar to HOL, and so of course doesn't appear in SOL or intuitionistic FOL.
@Dominic108 That's subjective. Like I said, birds and fishes. How about you spend some time studying intuitionistic logic first, and try to obtain your own 'structures' for it without looking at Kripke frames. Then only you can appreciate how non-trivial it is.
Entirely a side remark that I'm making because insomnia, I recently realized that sheaves on the Alexandrov topology of a poset are just S4 models for a free intuitionistic theory of pure equality. Which is pretty cute.
@user21820 I know you are away. So for next time, I want to say that your example HOL vs SOL explains what you mean by ad-hoc. Yes, but the same ideas are preserved as far as a way to interpret and talk about completeness and soundness are concerned. In both cases, we have a class of structures. Now I have to read about Intuitionistic logic and see why it is so different.
@MaliceVidrine By S4 models you mean Kripke frames for free intuitionistic theory of pure equality embedded in S4, right? By the way, do you know any interesting advantages of standard FOL over free FOL (admitting empty structures), besides the syntactic ones? I'm partial to the free variant, though it makes Skolemization messier.
And "quantifier elimination" would have to be renamed. =P
Are the concepts of signature (definitions of types of variables and constants), assignment (fct from the variables to the universes associated with each types) and structures (definitions of these universes + choice of constants) applicable to any logic? The definitions given in parenthesis are rough, but fill in your own formal definitions when answering.
@user21820 I just want to know what to expect when I will read about intuitionistic logic. Should I expect to see a signature for every intuitionistic logic? Same for assignments, etc.
@Dominic108 Of course they don't apply to every logic. That was my point right from the start.
As for intuitionistic logic, if you want a succinct presentation of a deductive system, you can start from this Fitch-style system and replace the ¬¬elim rule, namely ( ¬¬A ⊢ A ), by Ex Falso, namely ( ⊥ ⊢ A ). Everything else remains the same.
@user21820 The fact that some logic does not have a signature (even when we have some flexibility in the general, but fixed, concept of signature) or that for some other reason we cannot have assignments of variables into domains in structures to interpret the logic, surprises me a lot. It surprises me so much that I wonder, if we should not add such a requirement in the concept of logic. Is intuitionistic logic an example of a logic without a signature? That will be a choc for me.
Err.. so you haven't even read anything on intuitionistic logic? It has exactly the same syntax as classical logic, but really you should be reading about it first before making remarks on it. And quote whoever says it is a practical logic.
If it has the same syntax, then it must have a signature, because the signature is basically a set of types of variables. Also, if it is only that we replace a rule for LEM by something else (say, false implies every thing), then I think I have enough to understand some general points about it. Yes, I should not mention what others say that I do not understand. The fact is that "practical" is very large for me. If it describes weird applications, it has a chance of being practical.
A chance of being practical and practical is not so different.
Anyway, I am very surprise that some logic do not have a signature. The first thing I want to do is see a logic without a signature, because it's weird. It seems that intuitionistic is not an example, but I was just checking. I am lost when you say that some logic does not have a signature and cannot be interpreted in structures, even if we are flexible about the general, but fixed, definitions.
Of course, you understand that when I ask the question, I am not limited to a specific general notion of structures. What I mean is that FOL has structures, SOL has structures, HOL has structures, they have different kind of structures, but there is a general concept of structures behind all these cases. For me anything that allows to assign values to variables (given their types) qualifies as a structure.
So my question is what is an example of a logic without a signature? I especially want an example that has been considered and studied as a logic by many people in the scientific community.
You see I take time to decide what I want to study. This is something that I must determine myself. From what you are telling me, what I want to study is an example of a logic without signature, etc. and especially an example that has been considered and studied as a logic by many.
