8 ms·

Which formal logic do you suggest to replace it?

pdonis 6y ago
Second-order logic. (Not really to "replace", but to augment--to deal with those situations where first-order logic creates issues.) But I understand that not everyone would agree with that (apparently Scott Aaronson himself falls into this category, based on some of his comments in the comment section of the article).
- dwohnitmok 6y ago
  The traditional reason that logicians do not trust second-order logic is that usually attempts to try to formalize it start to lean back on first-order logic, e.g. by depending on a background theory of ZFC which is a first-order theory or via Henkin semantics which are also essentially first-order logic semantics and share all the same paradoxes of first-order logic. Hence the solutions that second-order logic presents to the issues of first-order logic are really just smoke and mirrors that fall apart and turn into the same problems of first-order logic on closer inspection.
  - andi999 6y ago
    Can you point me to (or explain briefly) what is second order logic?
    - yaantc 6y ago
      In first order logic one can only quantify over objects of the domain: in "for all x such that ..." the variable "x" represent an object. In second order logic, one can quantify over relations (and functions, sets...): "for all P such that ...". The wikipaedia page [1] has more details and is quite readable. Be careful about falling into a rabbit hole ;) [1] https://en.wikipedia.org/wiki/Second-order_logic https://en.wikipedia.org/wiki/Second-order_logic
      - andi999 6y ago
        Thanks, I will read that more. I am still confused, maybe you can tell me: for 'normal math'(what is usually taught in a formal 3 year degree), is first order logic enough (for getting all the results). What I am trying is to see where this second order logic fits in to what I use already.
        H8crilA 6y ago
        You can do a lot of math (almost all of it?) without ever touching logic. It's only important when you ask yourself things like "hmm, okay, the reals are closed under taking supremum of bounded sets, isn't that too much to ask for? how do I know reals are possible?". And of course the great logicians showed us that you can find "significant problems" already in natural numbers.
        andi999 6y ago
        Thats not what i meant. I mean certainly you are using some logic for doing math, do you agree with this? And if you agree, is the logic we use 1st or 1st and 1nd order?
        Kranar 6y ago
        The overwhelming majority of math is done using informal logic, similar to using pseudocode to describe an algorithm. Almost no one proves mathematical theorems using formal logic, whether it's first order logic or otherwise.
        yaantc 6y ago
        Normal practice is not that formal (except for logicians ;), but would definitely be second order logic. It's common to quantify over "all functions such that..." or over set of sets for example. Second order logic is more expressive.
        andi999 6y ago
        Thanks. I dont understand why for all elements of a set is first order and for all functions is second order - since functions (lets say R->R) are elements of the powerset of the cartesian product of RxR. So functions in math are usually part of first order logic, no?
- pron 6y ago
  Second-order logic is generally avoided in discussion of mathematical foundations because it is not very "foundational"; it is too vague or "mysterious" to serve as a comfortable foundation. Unlike FOL, it itself is incomplete. In a formal set theory, like ZFC, we postulate the existence of the set of natural numbers. This is something most logicians are comfortable with as being "mathematically foundational" ("God made the natural numbers; all else is the work of man"). Then, to describe the set of sets of natural numbers we use the powerset axiom that defines what exactly we mean by "all sets of natural numbers." Then, Löwenheim–Skolem appears and says that there are models of this set theory where the number of sets that satisfy this definition is countable (not inside the logic, but looking from the outside), to which we say: well, so be it. The reason this happens is because there is a fundamental limitation to the power of describing things using finite strings of symbols. Second-order can just say, no, when I say "all subsets" I mean absolutely all. But can we precisely formalise, i.e. write down in symbols, what we mean by "all" using some basic, "simple" foundation? The answer is no. Second-order logic just vaguely gestures toward "all" and says, "by all we mean all". It circumvents the limitations of formalisation -- i.e. describing things in finite sentences -- by alluding to non-describable things. Most logicians feel this isn't very foundational to rely on allusions to things that aren't themselves reducible to axioms in a basic foundation. Even when higher-order logics are used in formal mathematics, like various set theories or Isabelle's HOL, they are (at best) picked to be as powerful as (multi-sorted) FOL rather than "actual" SOL.
  - pdonis 6y ago
    > In a formal set theory, like ZFC, we postulate the existence of the set of natural numbers. But if your theory is a first-order theory, you cannot pin down "the set of natural numbers" to the one you and everyone else is actually thinking of; no matter what set of axioms you use to define "the set of natural numbers" (the Peano axioms, etc.), there will be semantic models other than the set of natural numbers you are thinking of that satisfy those axioms. The only way to precisely pin down "the set of natural numbers" to one semantic model--the one you actually want--is to use second-order logic. So it seems to me that there is a genuine tradeoff here. If you want enough expressive power to be able to precisely pin down what semantic model your theory is talking about, you need to accept that your theory will be making statements that are non-constructive--you can have an axiom that says every set has a power set, but you can't construct that power set in the general case. If you want your theory to be constructive, so that for every set that your theory says exists, you can see how to construct it explicitly, you need to accept that your theory will have multiple semantic models and only one of them is the one you want, and your theory can't pin it down for you.
paganel 6y ago
> Which formal logic do you suggest to replace it? Your question assumes that there's any "logic" to it all and that we should "replace" a "logic" by other "logic". That's a very strong assumption.
- bitdizzy 6y ago
  "... for the purposes of formalizing mathematical reasoning?"
  - paganel 6y ago
    From outside this all looks like “Glasperlenspiel” to me. That “mathematical reasoning” assumes that there should a “logic” behind its “operations”, but why should that be so it’s never told, it’s just assumed.
    - bitdizzy 6y ago
      Most modern mathematicians don't work with foundations but it was a hot topic at the beginning of the 20th century. Most mathematicians today wouldn't even be able to tell you when they are using the axiom of replacement, an important but technical piece of ZFC. Before the work on foundations mathematicians frequently relied on intuition to explain their ideas. The point of mathematical precision is to be able to transmit mathematical ideas with fidelity to other mathematicians; common intuitions are important for that even today. However, it is frequently the case that mathematical intuition breaks down and paradoxical ideas need to be reckoned with. One historical example is Weierstrass's "monster": a function that is everywhere continuous but nowhere differentiable. The intuition at the time was that a continuous function could only fail to be smooth at a set of isolated points, a very tame set. It is no coincidence that he came up with this example in a period when his school was trying to recast calculus on more rigorous footing. As for the motivation for founding mathematics on formal systems, it's because set theory is so useful for writing down mathematical ideas but naive set theory is plagued with contraditions, such Russel's paradox. Common language, too, is afflicted with contradictions such as Richard's paradox. The question was how to separate the wheat from the chaff so one does good mathematics and not nonsense. Influential mathematicians like Hilbert set out programs to establish set theory and arithmetic on a sound footing so that its use would not be held suspect. This required a more thorough mathematical development of logic as started by Boole, Frege, and others (my recollection of the precise history of these ideas is vague at this point). So concurrently we saw the mathematization of logic, arithmetic, and language and the establishment of a reasonable set theory that did not give rise to antinomies. None of the answers were entirely satisfactory but they were good enough that common mathematical activity could continue without too much doubt. When there are questions of precision, one tries to fall back on the informal mathematical language of sets which is commonly presumed to be formalizable in systems such as ZFC. A lot of development since then in formal mathematical systems has to do with the study of computation and the mechanization of mathematical reasoning.

Second-order logic. (Not really to "replace", but to augment--to deal with those situations where first-order logic creates issues.) But I understand that not everyone would agree with that (apparently Scott Aaronson himself falls into this category, based on some of his comments in the comment section of the article).

dwohnitmok 6y ago
The traditional reason that logicians do not trust second-order logic is that usually attempts to try to formalize it start to lean back on first-order logic, e.g. by depending on a background theory of ZFC which is a first-order theory or via Henkin semantics which are also essentially first-order logic semantics and share all the same paradoxes of first-order logic. Hence the solutions that second-order logic presents to the issues of first-order logic are really just smoke and mirrors that fall apart and turn into the same problems of first-order logic on closer inspection.
- andi999 6y ago
  Can you point me to (or explain briefly) what is second order logic?
  - yaantc 6y ago
    In first order logic one can only quantify over objects of the domain: in "for all x such that ..." the variable "x" represent an object. In second order logic, one can quantify over relations (and functions, sets...): "for all P such that ...". The wikipaedia page [1] has more details and is quite readable. Be careful about falling into a rabbit hole ;) [1] https://en.wikipedia.org/wiki/Second-order_logic https://en.wikipedia.org/wiki/Second-order_logic
    - andi999 6y ago
      Thanks, I will read that more. I am still confused, maybe you can tell me: for 'normal math'(what is usually taught in a formal 3 year degree), is first order logic enough (for getting all the results). What I am trying is to see where this second order logic fits in to what I use already.
      - H8crilA 6y ago
        You can do a lot of math (almost all of it?) without ever touching logic. It's only important when you ask yourself things like "hmm, okay, the reals are closed under taking supremum of bounded sets, isn't that too much to ask for? how do I know reals are possible?". And of course the great logicians showed us that you can find "significant problems" already in natural numbers.
        andi999 6y ago
        Thats not what i meant. I mean certainly you are using some logic for doing math, do you agree with this? And if you agree, is the logic we use 1st or 1st and 1nd order?
        Kranar 6y ago
        The overwhelming majority of math is done using informal logic, similar to using pseudocode to describe an algorithm. Almost no one proves mathematical theorems using formal logic, whether it's first order logic or otherwise.
      - yaantc 6y ago
        Normal practice is not that formal (except for logicians ;), but would definitely be second order logic. It's common to quantify over "all functions such that..." or over set of sets for example. Second order logic is more expressive.
        andi999 6y ago
        Thanks. I dont understand why for all elements of a set is first order and for all functions is second order - since functions (lets say R->R) are elements of the powerset of the cartesian product of RxR. So functions in math are usually part of first order logic, no?
pron 6y ago
Second-order logic is generally avoided in discussion of mathematical foundations because it is not very "foundational"; it is too vague or "mysterious" to serve as a comfortable foundation. Unlike FOL, it itself is incomplete. In a formal set theory, like ZFC, we postulate the existence of the set of natural numbers. This is something most logicians are comfortable with as being "mathematically foundational" ("God made the natural numbers; all else is the work of man"). Then, to describe the set of sets of natural numbers we use the powerset axiom that defines what exactly we mean by "all sets of natural numbers." Then, Löwenheim–Skolem appears and says that there are models of this set theory where the number of sets that satisfy this definition is countable (not inside the logic, but looking from the outside), to which we say: well, so be it. The reason this happens is because there is a fundamental limitation to the power of describing things using finite strings of symbols. Second-order can just say, no, when I say "all subsets" I mean absolutely all. But can we precisely formalise, i.e. write down in symbols, what we mean by "all" using some basic, "simple" foundation? The answer is no. Second-order logic just vaguely gestures toward "all" and says, "by all we mean all". It circumvents the limitations of formalisation -- i.e. describing things in finite sentences -- by alluding to non-describable things. Most logicians feel this isn't very foundational to rely on allusions to things that aren't themselves reducible to axioms in a basic foundation. Even when higher-order logics are used in formal mathematics, like various set theories or Isabelle's HOL, they are (at best) picked to be as powerful as (multi-sorted) FOL rather than "actual" SOL.
- pdonis 6y ago
  > In a formal set theory, like ZFC, we postulate the existence of the set of natural numbers. But if your theory is a first-order theory, you cannot pin down "the set of natural numbers" to the one you and everyone else is actually thinking of; no matter what set of axioms you use to define "the set of natural numbers" (the Peano axioms, etc.), there will be semantic models other than the set of natural numbers you are thinking of that satisfy those axioms. The only way to precisely pin down "the set of natural numbers" to one semantic model--the one you actually want--is to use second-order logic. So it seems to me that there is a genuine tradeoff here. If you want enough expressive power to be able to precisely pin down what semantic model your theory is talking about, you need to accept that your theory will be making statements that are non-constructive--you can have an axiom that says every set has a power set, but you can't construct that power set in the general case. If you want your theory to be constructive, so that for every set that your theory says exists, you can see how to construct it explicitly, you need to accept that your theory will have multiple semantic models and only one of them is the one you want, and your theory can't pin it down for you.

paganel 6y ago

> Which formal logic do you suggest to replace it? Your question assumes that there's any "logic" to it all and that we should "replace" a "logic" by other "logic". That's a very strong assumption.

bitdizzy 6y ago
"... for the purposes of formalizing mathematical reasoning?"
- paganel 6y ago
  From outside this all looks like “Glasperlenspiel” to me. That “mathematical reasoning” assumes that there should a “logic” behind its “operations”, but why should that be so it’s never told, it’s just assumed.
  - bitdizzy 6y ago
    Most modern mathematicians don't work with foundations but it was a hot topic at the beginning of the 20th century. Most mathematicians today wouldn't even be able to tell you when they are using the axiom of replacement, an important but technical piece of ZFC. Before the work on foundations mathematicians frequently relied on intuition to explain their ideas. The point of mathematical precision is to be able to transmit mathematical ideas with fidelity to other mathematicians; common intuitions are important for that even today. However, it is frequently the case that mathematical intuition breaks down and paradoxical ideas need to be reckoned with. One historical example is Weierstrass's "monster": a function that is everywhere continuous but nowhere differentiable. The intuition at the time was that a continuous function could only fail to be smooth at a set of isolated points, a very tame set. It is no coincidence that he came up with this example in a period when his school was trying to recast calculus on more rigorous footing. As for the motivation for founding mathematics on formal systems, it's because set theory is so useful for writing down mathematical ideas but naive set theory is plagued with contraditions, such Russel's paradox. Common language, too, is afflicted with contradictions such as Richard's paradox. The question was how to separate the wheat from the chaff so one does good mathematics and not nonsense. Influential mathematicians like Hilbert set out programs to establish set theory and arithmetic on a sound footing so that its use would not be held suspect. This required a more thorough mathematical development of logic as started by Boole, Frege, and others (my recollection of the precise history of these ideas is vague at this point). So concurrently we saw the mathematization of logic, arithmetic, and language and the establishment of a reasonable set theory that did not give rise to antinomies. None of the answers were entirely satisfactory but they were good enough that common mathematical activity could continue without too much doubt. When there are questions of precision, one tries to fall back on the informal mathematical language of sets which is commonly presumed to be formalizable in systems such as ZFC. A lot of development since then in formal mathematical systems has to do with the study of computation and the mechanization of mathematical reasoning.