4 ms·

> whether any given formal system actually is consistent is not dependent on consensus, it is a fact, either true or false, completely independent of consensus.

> whether any given formal system actually is consistent is not dependent on consensus, it is a fact, either true or false, completely independent of consensus. The definition of "consistent" seems completely entangled with a given social group's ideas of "rational". You might imply that our word for it hints at a Platonic ideal of "consistent", but if that's true, then you're caught in an infinite cascade of which nuances of meaning between the Platonic Ideal and our concrete reality are actually reflections of the truth or corruption of it.

prmph 4y ago
Exactly the point I was making. Many do not seems to see the fundamental issue at play here, and another way to think of them is what you have hinted at: the role of language. There is no objective way to nail down the meaning of words, like "consistent", "proof", "equal", etc. Suppose one wanted a maximally rigorous definition of "equal". Does it mean two things that cause people to think of the same thing when they are mentioned? Does it mean two things that occupy the same position in space at all times? It is actually a difficult concept to define rigorously. This is not to deny that there is an objective reality. But that reality is highly contextual and multi-faceted. We cannot be 100% exact in defining that reality using language (even a math language), and this is where the social nature of that reality becomes apparent. The role of proofs are in creating, as far as possible, as rigorous a shared context for the reality being described.
- auggierose 4y ago
  Equality is actually quite easy to axiomatise in most logics, here in my favourite logic: 1) x = x 2) x = y => P[x] => P[y] In my opinion, there is a mathematical reality, which is shared by everyone, even by those who don't believe in it :-) For example, a logical system exists in that reality, and you can either derive a theorem in that system or not in this reality. I don't think it is possible that there is a third possibility. I don't think it is possible that I have a different reality from you in that respect. This reality is not socially constructed, it just is. Intuitionism will tell you that because you don't know if a certain theorem is derivable, it is in some sort of hybrid state until we know for sure via a intuitionistic proof or a counter example. I think that is bullocks. Either there is a proof or not. Either there is a counter example, or not. Beyond that, extending this mathematical reality, there is a wider, not as easily accessible reality. We can try to understand that reality by modelling it via certain assumptions, and then applying our mathematical reality to those assumptions. I believe the mathematical conclusions we draw from this will be real to the extent that the assumptions are true; but of course you cannot ever be sure about those assumptions, and so you cannot be sure about the conclusions. But if you notice that your conclusions do not hold, you need to challenge your assumptions, not your mathematics.
  - prmph 4y ago
    Can you put into words the symbolic notation you have in your comment? I think I understand pretty well what you mean, but for the avoidance of doubt, explain what the notation means, and then I will indicate all the assumptions on which it is relying.
    - auggierose 4y ago
      It would be somewhat lengthy to explain its meaning exactly here. You can read about its exact meaning and its context here: https://doi.org/10.47757/pal.2 https://doi.org/10.47757/pal.2 In short what it usually means (the exact meaning depends on the model under consideration) is that there is a binary operation "=", such that "x = x" is a theorem, that is evaluating "x = x" will evaluate to "true" for any object x in the mathematical universe. Furthermore, for any unary proper operator "P", and any two objects x and y of the mathematical universe, the expression "(x = y) => (P[x] => P[y])" will also evaluate to "true". Here "=>" is another binary operation called implication, which has some special properties outlined in the link. P[x] denotes the application of the operator P to the object x. Edit: Oh, forgot to add the third axiom for equality (it is actually more an axiom about "true", but uses equality): 3) A => (A = true) What this means is that for any object A of the mathematical universe, if you evaluate "A => (A = true)", you obtain the value "true".
- naasking 4y ago
  Have you perchance been reading a lot of Wittgenstein? I think you're conflating universality and objectivity. Those terms you list all have objective definitions, but the specific characteristics they have in any given logic may differ. That means they are not universal, but that doesn't make them non-objective. Objective typically means "mind independent". Your example of equality already demonstrates you understand equality's objective definition: you implicitly operate on the notion that "equality" means some form of equivalence, some ability to substitute B for C in a specific context that results in no observable/expressible change. That is an informal but objective understanding of equality. What you're recognizing is that equality can have different logical properties in different contexts, where "context" can be understood as the formal language we're using, ie. it's not universal. But it's role in any given logic is always the same and not dependent on the provers mind state or his surrounding culture, ie. it is objective. Godel showed that there is no such thing as a universal logic in our current approach to formal systems, but that didn't suddenly make logic non-objective. It simply means that there is no Ur-logic that can subsume all other logics (which is why most assert that Godel ended Hilbert's program). So what logics a culture or species may use or find interesting, and the process by which they explore these systems are socially contextual, but the structures themselves and their internal consistency is not socially constructed. A culture can certainly believe a formal system they use to be logically consistent, but that's no more interesting a statement than that some cultures believed that Thor caused lightning. In other words, they could just be wrong about the consistency of their arguments.
  - auggierose 4y ago
    > Godel showed that there is no such thing as a universal logic in our current approach to formal systems, but that didn't suddenly make logic non-objective. It simply means that there is no Ur-logic that can subsume all other logics (which is why most assert that Godel ended Hilbert's program). Could you elaborate on that? Any references?
    - naasking 4y ago
      These are the implications of Godel's incompleteness theorems. No formal system expressive enough to encode arithmetic can simultaneously be both complete and prove its own consistency, because there will always be true propositions expressible in that system that cannot be proven in that system. This is why Hilbert's program to finitely axiomatize mathematics can't be completed. The "escape hatch" here is simply that not all propositions are actually interesting, so finite axiomatizations are still very useful, and we can extend the axiomatic basis as needed given satisfactory justification. This last part is the only place where social consensus sometimes comes into play (continuum hypothesis, etc). Edit: there is another possible escape hatch that hasn't been fully explored IMO, and that's some variant of finitism. All these impossibility proofs depend on infinite structures to derive incompleteness or contradiction, but if infinite structures are not expressible...
auggierose 4y ago
There is a simple definition for what consistent means, which naasking is referring to: is it impossible to derive "false" purely by applying the rules of the logical system?
- prmph 4y ago
  "False" is meaningless in a logic system that relies on probabilities in stead or true/false. Even in our commonly used logic system, what does false actually mean?
  - auggierose 4y ago
    I can point you to my favourite logic ;-) Here false is defined as false = (∀x. x) So in this case, it derives its meaning from whatever the meaning of the ∀ operator is. Its meaning is the result of applying the ∀ operator to the identity operation. Nobody is questioning that there are different possibilities for logical systems, and different possible semantics for them. The choice of logical system is up to you, and ultimately, part of your assumptions. A proof assistant uses a fixed logical system, and your mathematics needs to fit into this system to be expressible in the proof assistant. Apart from my favourite logic, there are several well-known logical systems commonly assumed to be able to represent all of mathematics more or less faithfully: first-order logic, simply-typed higher-order logic, and dependent type theory. What I like about my favourite logic is that I believe that all other logics, even quantum logics, can be expressed in it in a straightforward way. This has the advantage that once you expressed your logic in this way, you get the meaning of it for free. Of course, you still need to make sure that this is the intended meaning.
    - musingsole 4y ago
      You draw lines and insist there's no space between them.
      - auggierose 4y ago
        Not sure what you are trying to say. Care to elaborate?

prmph 4y ago

Exactly the point I was making. Many do not seems to see the fundamental issue at play here, and another way to think of them is what you have hinted at: the role of language. There is no objective way to nail down the meaning of words, like "consistent", "proof", "equal", etc. Suppose one wanted a maximally rigorous definition of "equal". Does it mean two things that cause people to think of the same thing when they are mentioned? Does it mean two things that occupy the same position in space at all times? It is actually a difficult concept to define rigorously. This is not to deny that there is an objective reality. But that reality is highly contextual and multi-faceted. We cannot be 100% exact in defining that reality using language (even a math language), and this is where the social nature of that reality becomes apparent. The role of proofs are in creating, as far as possible, as rigorous a shared context for the reality being described.

auggierose 4y ago
Equality is actually quite easy to axiomatise in most logics, here in my favourite logic: 1) x = x 2) x = y => P[x] => P[y] In my opinion, there is a mathematical reality, which is shared by everyone, even by those who don't believe in it :-) For example, a logical system exists in that reality, and you can either derive a theorem in that system or not in this reality. I don't think it is possible that there is a third possibility. I don't think it is possible that I have a different reality from you in that respect. This reality is not socially constructed, it just is. Intuitionism will tell you that because you don't know if a certain theorem is derivable, it is in some sort of hybrid state until we know for sure via a intuitionistic proof or a counter example. I think that is bullocks. Either there is a proof or not. Either there is a counter example, or not. Beyond that, extending this mathematical reality, there is a wider, not as easily accessible reality. We can try to understand that reality by modelling it via certain assumptions, and then applying our mathematical reality to those assumptions. I believe the mathematical conclusions we draw from this will be real to the extent that the assumptions are true; but of course you cannot ever be sure about those assumptions, and so you cannot be sure about the conclusions. But if you notice that your conclusions do not hold, you need to challenge your assumptions, not your mathematics.
- prmph 4y ago
  Can you put into words the symbolic notation you have in your comment? I think I understand pretty well what you mean, but for the avoidance of doubt, explain what the notation means, and then I will indicate all the assumptions on which it is relying.
  - auggierose 4y ago
    It would be somewhat lengthy to explain its meaning exactly here. You can read about its exact meaning and its context here: https://doi.org/10.47757/pal.2 https://doi.org/10.47757/pal.2 In short what it usually means (the exact meaning depends on the model under consideration) is that there is a binary operation "=", such that "x = x" is a theorem, that is evaluating "x = x" will evaluate to "true" for any object x in the mathematical universe. Furthermore, for any unary proper operator "P", and any two objects x and y of the mathematical universe, the expression "(x = y) => (P[x] => P[y])" will also evaluate to "true". Here "=>" is another binary operation called implication, which has some special properties outlined in the link. P[x] denotes the application of the operator P to the object x. Edit: Oh, forgot to add the third axiom for equality (it is actually more an axiom about "true", but uses equality): 3) A => (A = true) What this means is that for any object A of the mathematical universe, if you evaluate "A => (A = true)", you obtain the value "true".
naasking 4y ago
Have you perchance been reading a lot of Wittgenstein? I think you're conflating universality and objectivity. Those terms you list all have objective definitions, but the specific characteristics they have in any given logic may differ. That means they are not universal, but that doesn't make them non-objective. Objective typically means "mind independent". Your example of equality already demonstrates you understand equality's objective definition: you implicitly operate on the notion that "equality" means some form of equivalence, some ability to substitute B for C in a specific context that results in no observable/expressible change. That is an informal but objective understanding of equality. What you're recognizing is that equality can have different logical properties in different contexts, where "context" can be understood as the formal language we're using, ie. it's not universal. But it's role in any given logic is always the same and not dependent on the provers mind state or his surrounding culture, ie. it is objective. Godel showed that there is no such thing as a universal logic in our current approach to formal systems, but that didn't suddenly make logic non-objective. It simply means that there is no Ur-logic that can subsume all other logics (which is why most assert that Godel ended Hilbert's program). So what logics a culture or species may use or find interesting, and the process by which they explore these systems are socially contextual, but the structures themselves and their internal consistency is not socially constructed. A culture can certainly believe a formal system they use to be logically consistent, but that's no more interesting a statement than that some cultures believed that Thor caused lightning. In other words, they could just be wrong about the consistency of their arguments.
- auggierose 4y ago
  > Godel showed that there is no such thing as a universal logic in our current approach to formal systems, but that didn't suddenly make logic non-objective. It simply means that there is no Ur-logic that can subsume all other logics (which is why most assert that Godel ended Hilbert's program). Could you elaborate on that? Any references?
  - naasking 4y ago
    These are the implications of Godel's incompleteness theorems. No formal system expressive enough to encode arithmetic can simultaneously be both complete and prove its own consistency, because there will always be true propositions expressible in that system that cannot be proven in that system. This is why Hilbert's program to finitely axiomatize mathematics can't be completed. The "escape hatch" here is simply that not all propositions are actually interesting, so finite axiomatizations are still very useful, and we can extend the axiomatic basis as needed given satisfactory justification. This last part is the only place where social consensus sometimes comes into play (continuum hypothesis, etc). Edit: there is another possible escape hatch that hasn't been fully explored IMO, and that's some variant of finitism. All these impossibility proofs depend on infinite structures to derive incompleteness or contradiction, but if infinite structures are not expressible...

auggierose 4y ago

There is a simple definition for what consistent means, which naasking is referring to: is it impossible to derive "false" purely by applying the rules of the logical system?

prmph 4y ago
"False" is meaningless in a logic system that relies on probabilities in stead or true/false. Even in our commonly used logic system, what does false actually mean?
- auggierose 4y ago
  I can point you to my favourite logic ;-) Here false is defined as false = (∀x. x) So in this case, it derives its meaning from whatever the meaning of the ∀ operator is. Its meaning is the result of applying the ∀ operator to the identity operation. Nobody is questioning that there are different possibilities for logical systems, and different possible semantics for them. The choice of logical system is up to you, and ultimately, part of your assumptions. A proof assistant uses a fixed logical system, and your mathematics needs to fit into this system to be expressible in the proof assistant. Apart from my favourite logic, there are several well-known logical systems commonly assumed to be able to represent all of mathematics more or less faithfully: first-order logic, simply-typed higher-order logic, and dependent type theory. What I like about my favourite logic is that I believe that all other logics, even quantum logics, can be expressed in it in a straightforward way. This has the advantage that once you expressed your logic in this way, you get the meaning of it for free. Of course, you still need to make sure that this is the intended meaning.
  - musingsole 4y ago
    You draw lines and insist there's no space between them.
    - auggierose 4y ago
      Not sure what you are trying to say. Care to elaborate?