Logic with “co-relations” - sources?Most general formulation of Gödel's incompleteness theoremsThe sets in mathematical logicAxiomatization of first order logic (finitely many variables)What is the role of the (formalized) omega rule in Ramified Analysis?Function extensionality: does it make a difference? why would one keep it out of the axioms?Is Girard's LU just an embedding of classical and intuitionistic logic into linear logic?Adding nonconstructive disjunction to intuitionistic logicIs this kind of predication preserved under co-extensionality?Mathematics without the principle of unique choiceDifferences between logic with and without equality

Logic with “co-relations” - sources?


Most general formulation of Gödel's incompleteness theoremsThe sets in mathematical logicAxiomatization of first order logic (finitely many variables)What is the role of the (formalized) omega rule in Ramified Analysis?Function extensionality: does it make a difference? why would one keep it out of the axioms?Is Girard's LU just an embedding of classical and intuitionistic logic into linear logic?Adding nonconstructive disjunction to intuitionistic logicIs this kind of predication preserved under co-extensionality?Mathematics without the principle of unique choiceDifferences between logic with and without equality













5












$begingroup$


My question is on a seemingly-natural extension of classical logic that I've been playing around with a bit in the context of generalized recursion theory. I'm sure it's been treated extensively already, but my literature search skills have failed me.




What is a good source on what happens when we extend first-order logic (or other logics, for that matter) to allow "co-relations?"




By "co-relation" I mean a syntactic object which behaves dually to a relation: rather than taking some terms and producing a formula, a co-relation should take some formulas and produce a term. The motivating example of a co-relation is of course Godel numbering, but there are other reasonable examples as well (EDIT: see Andreas Blass' comment below).



To clarify: while I'm definitely interested in examples, what I'm looking for in an answer is something approaching a general theory, at least the basics of such - in particular, it should treat arbitrary signatures involving constants, functions, relations, and co-relations, and be able to make sense of arbitrary theories in such signatures. So an example of a specific theory involving co-relations is not what I'm looking for.




It's worth pointing out - and this may also help motivate the question - that there are real issues in setting up the semantics for logic with co-relations (EDIT: and see Andrej Bauer's comment below). The most significant issue, I think, is how quantifiers can or cannot "reach into" co-predicates. Look at $(mathbbN;+,cdot,G)$ where $G$ is an appropriate Godel-numbering co-relation. Suppose the Godel number of the formula "$x=x$" is $17$, and for each numeral $underlinen$ the Godel number of the sentence "$underlinen=underlinen$" is $3n$. Then is $forall x(G(x=x)=underline17)$ true, or is $forall x(G(x=x)=underline3cdot x)$ true? I have my own guess about the "right" way to set things up, but I wouldn't be surprised at all to learn that I'm going about things incorrectly, so I'm leaving the question fairly broad.



FINAL EDIT: One key aspect here is that I am in no way demanding extensionality - co-relations are not restricted in any way in terms of how they behave on logically equivalent (tuples of) formulas. (This is of course necessary if Godel numbering is to be an example, after all.)










share|cite|improve this question











$endgroup$











  • $begingroup$
    The "computer science" tag is a guess on my part - I vaguely recall seeing something like this in the theoretical computer science literature, but I couldn't track it down so I'm not sure. If it seems inappropriate, feel free to remove it.
    $endgroup$
    – Noah Schweber
    5 hours ago






  • 2




    $begingroup$
    At least some of the mysteries you've encountered would be dispelled if you treated syntax properly (by having terms and formulas appear in variable contexts), and you paid attention between meta-syntax and object-level syntax. Computer scientists have done this sort of thing, but you simply will have to get used to more structure than is available with ad-hoc techniues such as Gödel numberings. If that's acceptable, I can give some references.
    $endgroup$
    – Andrej Bauer
    5 hours ago










  • $begingroup$
    How rigid is the notion of correlation? Do you want it to act on "pure" formulas (e.g. some syntactic elements that do not contain symbols for any corelation)? Does a corelation have an arity (Goedel numbering is unary; do you have binary examples or ideas for corelations without a fixed arity)? If I saw more, I might recall something from the Universal Algebra. Since you are looking for a dual, one tactic is to hope for some form of Galois connection and look for literature involving your notion and a Galois connection. Gerhard "Or Combine With Other Ingredients" Paseman, 2019.03.18.
    $endgroup$
    – Gerhard Paseman
    5 hours ago






  • 2




    $begingroup$
    Would your co-relations include things like set-comprehension, where $x:phi(x)$ is a term produced from a formula $phi(x)$? If so, then probably you'd also include things like $lambda$-abstraction and Hilbert's $epsilon$ operator.
    $endgroup$
    – Andreas Blass
    5 hours ago










  • $begingroup$
    @AndrejBauer Yes please, that's more than acceptable! (And I think I'm already thinking along those lines, but laboriously and inefficiently.)
    $endgroup$
    – Noah Schweber
    5 hours ago
















5












$begingroup$


My question is on a seemingly-natural extension of classical logic that I've been playing around with a bit in the context of generalized recursion theory. I'm sure it's been treated extensively already, but my literature search skills have failed me.




What is a good source on what happens when we extend first-order logic (or other logics, for that matter) to allow "co-relations?"




By "co-relation" I mean a syntactic object which behaves dually to a relation: rather than taking some terms and producing a formula, a co-relation should take some formulas and produce a term. The motivating example of a co-relation is of course Godel numbering, but there are other reasonable examples as well (EDIT: see Andreas Blass' comment below).



To clarify: while I'm definitely interested in examples, what I'm looking for in an answer is something approaching a general theory, at least the basics of such - in particular, it should treat arbitrary signatures involving constants, functions, relations, and co-relations, and be able to make sense of arbitrary theories in such signatures. So an example of a specific theory involving co-relations is not what I'm looking for.




It's worth pointing out - and this may also help motivate the question - that there are real issues in setting up the semantics for logic with co-relations (EDIT: and see Andrej Bauer's comment below). The most significant issue, I think, is how quantifiers can or cannot "reach into" co-predicates. Look at $(mathbbN;+,cdot,G)$ where $G$ is an appropriate Godel-numbering co-relation. Suppose the Godel number of the formula "$x=x$" is $17$, and for each numeral $underlinen$ the Godel number of the sentence "$underlinen=underlinen$" is $3n$. Then is $forall x(G(x=x)=underline17)$ true, or is $forall x(G(x=x)=underline3cdot x)$ true? I have my own guess about the "right" way to set things up, but I wouldn't be surprised at all to learn that I'm going about things incorrectly, so I'm leaving the question fairly broad.



FINAL EDIT: One key aspect here is that I am in no way demanding extensionality - co-relations are not restricted in any way in terms of how they behave on logically equivalent (tuples of) formulas. (This is of course necessary if Godel numbering is to be an example, after all.)










share|cite|improve this question











$endgroup$











  • $begingroup$
    The "computer science" tag is a guess on my part - I vaguely recall seeing something like this in the theoretical computer science literature, but I couldn't track it down so I'm not sure. If it seems inappropriate, feel free to remove it.
    $endgroup$
    – Noah Schweber
    5 hours ago






  • 2




    $begingroup$
    At least some of the mysteries you've encountered would be dispelled if you treated syntax properly (by having terms and formulas appear in variable contexts), and you paid attention between meta-syntax and object-level syntax. Computer scientists have done this sort of thing, but you simply will have to get used to more structure than is available with ad-hoc techniues such as Gödel numberings. If that's acceptable, I can give some references.
    $endgroup$
    – Andrej Bauer
    5 hours ago










  • $begingroup$
    How rigid is the notion of correlation? Do you want it to act on "pure" formulas (e.g. some syntactic elements that do not contain symbols for any corelation)? Does a corelation have an arity (Goedel numbering is unary; do you have binary examples or ideas for corelations without a fixed arity)? If I saw more, I might recall something from the Universal Algebra. Since you are looking for a dual, one tactic is to hope for some form of Galois connection and look for literature involving your notion and a Galois connection. Gerhard "Or Combine With Other Ingredients" Paseman, 2019.03.18.
    $endgroup$
    – Gerhard Paseman
    5 hours ago






  • 2




    $begingroup$
    Would your co-relations include things like set-comprehension, where $x:phi(x)$ is a term produced from a formula $phi(x)$? If so, then probably you'd also include things like $lambda$-abstraction and Hilbert's $epsilon$ operator.
    $endgroup$
    – Andreas Blass
    5 hours ago










  • $begingroup$
    @AndrejBauer Yes please, that's more than acceptable! (And I think I'm already thinking along those lines, but laboriously and inefficiently.)
    $endgroup$
    – Noah Schweber
    5 hours ago














5












5








5





$begingroup$


My question is on a seemingly-natural extension of classical logic that I've been playing around with a bit in the context of generalized recursion theory. I'm sure it's been treated extensively already, but my literature search skills have failed me.




What is a good source on what happens when we extend first-order logic (or other logics, for that matter) to allow "co-relations?"




By "co-relation" I mean a syntactic object which behaves dually to a relation: rather than taking some terms and producing a formula, a co-relation should take some formulas and produce a term. The motivating example of a co-relation is of course Godel numbering, but there are other reasonable examples as well (EDIT: see Andreas Blass' comment below).



To clarify: while I'm definitely interested in examples, what I'm looking for in an answer is something approaching a general theory, at least the basics of such - in particular, it should treat arbitrary signatures involving constants, functions, relations, and co-relations, and be able to make sense of arbitrary theories in such signatures. So an example of a specific theory involving co-relations is not what I'm looking for.




It's worth pointing out - and this may also help motivate the question - that there are real issues in setting up the semantics for logic with co-relations (EDIT: and see Andrej Bauer's comment below). The most significant issue, I think, is how quantifiers can or cannot "reach into" co-predicates. Look at $(mathbbN;+,cdot,G)$ where $G$ is an appropriate Godel-numbering co-relation. Suppose the Godel number of the formula "$x=x$" is $17$, and for each numeral $underlinen$ the Godel number of the sentence "$underlinen=underlinen$" is $3n$. Then is $forall x(G(x=x)=underline17)$ true, or is $forall x(G(x=x)=underline3cdot x)$ true? I have my own guess about the "right" way to set things up, but I wouldn't be surprised at all to learn that I'm going about things incorrectly, so I'm leaving the question fairly broad.



FINAL EDIT: One key aspect here is that I am in no way demanding extensionality - co-relations are not restricted in any way in terms of how they behave on logically equivalent (tuples of) formulas. (This is of course necessary if Godel numbering is to be an example, after all.)










share|cite|improve this question











$endgroup$




My question is on a seemingly-natural extension of classical logic that I've been playing around with a bit in the context of generalized recursion theory. I'm sure it's been treated extensively already, but my literature search skills have failed me.




What is a good source on what happens when we extend first-order logic (or other logics, for that matter) to allow "co-relations?"




By "co-relation" I mean a syntactic object which behaves dually to a relation: rather than taking some terms and producing a formula, a co-relation should take some formulas and produce a term. The motivating example of a co-relation is of course Godel numbering, but there are other reasonable examples as well (EDIT: see Andreas Blass' comment below).



To clarify: while I'm definitely interested in examples, what I'm looking for in an answer is something approaching a general theory, at least the basics of such - in particular, it should treat arbitrary signatures involving constants, functions, relations, and co-relations, and be able to make sense of arbitrary theories in such signatures. So an example of a specific theory involving co-relations is not what I'm looking for.




It's worth pointing out - and this may also help motivate the question - that there are real issues in setting up the semantics for logic with co-relations (EDIT: and see Andrej Bauer's comment below). The most significant issue, I think, is how quantifiers can or cannot "reach into" co-predicates. Look at $(mathbbN;+,cdot,G)$ where $G$ is an appropriate Godel-numbering co-relation. Suppose the Godel number of the formula "$x=x$" is $17$, and for each numeral $underlinen$ the Godel number of the sentence "$underlinen=underlinen$" is $3n$. Then is $forall x(G(x=x)=underline17)$ true, or is $forall x(G(x=x)=underline3cdot x)$ true? I have my own guess about the "right" way to set things up, but I wouldn't be surprised at all to learn that I'm going about things incorrectly, so I'm leaving the question fairly broad.



FINAL EDIT: One key aspect here is that I am in no way demanding extensionality - co-relations are not restricted in any way in terms of how they behave on logically equivalent (tuples of) formulas. (This is of course necessary if Godel numbering is to be an example, after all.)







reference-request lo.logic computer-science proof-theory foundations






share|cite|improve this question















share|cite|improve this question













share|cite|improve this question




share|cite|improve this question








edited 3 hours ago







Noah Schweber

















asked 5 hours ago









Noah SchweberNoah Schweber

19.3k349146




19.3k349146











  • $begingroup$
    The "computer science" tag is a guess on my part - I vaguely recall seeing something like this in the theoretical computer science literature, but I couldn't track it down so I'm not sure. If it seems inappropriate, feel free to remove it.
    $endgroup$
    – Noah Schweber
    5 hours ago






  • 2




    $begingroup$
    At least some of the mysteries you've encountered would be dispelled if you treated syntax properly (by having terms and formulas appear in variable contexts), and you paid attention between meta-syntax and object-level syntax. Computer scientists have done this sort of thing, but you simply will have to get used to more structure than is available with ad-hoc techniues such as Gödel numberings. If that's acceptable, I can give some references.
    $endgroup$
    – Andrej Bauer
    5 hours ago










  • $begingroup$
    How rigid is the notion of correlation? Do you want it to act on "pure" formulas (e.g. some syntactic elements that do not contain symbols for any corelation)? Does a corelation have an arity (Goedel numbering is unary; do you have binary examples or ideas for corelations without a fixed arity)? If I saw more, I might recall something from the Universal Algebra. Since you are looking for a dual, one tactic is to hope for some form of Galois connection and look for literature involving your notion and a Galois connection. Gerhard "Or Combine With Other Ingredients" Paseman, 2019.03.18.
    $endgroup$
    – Gerhard Paseman
    5 hours ago






  • 2




    $begingroup$
    Would your co-relations include things like set-comprehension, where $x:phi(x)$ is a term produced from a formula $phi(x)$? If so, then probably you'd also include things like $lambda$-abstraction and Hilbert's $epsilon$ operator.
    $endgroup$
    – Andreas Blass
    5 hours ago










  • $begingroup$
    @AndrejBauer Yes please, that's more than acceptable! (And I think I'm already thinking along those lines, but laboriously and inefficiently.)
    $endgroup$
    – Noah Schweber
    5 hours ago

















  • $begingroup$
    The "computer science" tag is a guess on my part - I vaguely recall seeing something like this in the theoretical computer science literature, but I couldn't track it down so I'm not sure. If it seems inappropriate, feel free to remove it.
    $endgroup$
    – Noah Schweber
    5 hours ago






  • 2




    $begingroup$
    At least some of the mysteries you've encountered would be dispelled if you treated syntax properly (by having terms and formulas appear in variable contexts), and you paid attention between meta-syntax and object-level syntax. Computer scientists have done this sort of thing, but you simply will have to get used to more structure than is available with ad-hoc techniues such as Gödel numberings. If that's acceptable, I can give some references.
    $endgroup$
    – Andrej Bauer
    5 hours ago










  • $begingroup$
    How rigid is the notion of correlation? Do you want it to act on "pure" formulas (e.g. some syntactic elements that do not contain symbols for any corelation)? Does a corelation have an arity (Goedel numbering is unary; do you have binary examples or ideas for corelations without a fixed arity)? If I saw more, I might recall something from the Universal Algebra. Since you are looking for a dual, one tactic is to hope for some form of Galois connection and look for literature involving your notion and a Galois connection. Gerhard "Or Combine With Other Ingredients" Paseman, 2019.03.18.
    $endgroup$
    – Gerhard Paseman
    5 hours ago






  • 2




    $begingroup$
    Would your co-relations include things like set-comprehension, where $x:phi(x)$ is a term produced from a formula $phi(x)$? If so, then probably you'd also include things like $lambda$-abstraction and Hilbert's $epsilon$ operator.
    $endgroup$
    – Andreas Blass
    5 hours ago










  • $begingroup$
    @AndrejBauer Yes please, that's more than acceptable! (And I think I'm already thinking along those lines, but laboriously and inefficiently.)
    $endgroup$
    – Noah Schweber
    5 hours ago
















$begingroup$
The "computer science" tag is a guess on my part - I vaguely recall seeing something like this in the theoretical computer science literature, but I couldn't track it down so I'm not sure. If it seems inappropriate, feel free to remove it.
$endgroup$
– Noah Schweber
5 hours ago




$begingroup$
The "computer science" tag is a guess on my part - I vaguely recall seeing something like this in the theoretical computer science literature, but I couldn't track it down so I'm not sure. If it seems inappropriate, feel free to remove it.
$endgroup$
– Noah Schweber
5 hours ago




2




2




$begingroup$
At least some of the mysteries you've encountered would be dispelled if you treated syntax properly (by having terms and formulas appear in variable contexts), and you paid attention between meta-syntax and object-level syntax. Computer scientists have done this sort of thing, but you simply will have to get used to more structure than is available with ad-hoc techniues such as Gödel numberings. If that's acceptable, I can give some references.
$endgroup$
– Andrej Bauer
5 hours ago




$begingroup$
At least some of the mysteries you've encountered would be dispelled if you treated syntax properly (by having terms and formulas appear in variable contexts), and you paid attention between meta-syntax and object-level syntax. Computer scientists have done this sort of thing, but you simply will have to get used to more structure than is available with ad-hoc techniues such as Gödel numberings. If that's acceptable, I can give some references.
$endgroup$
– Andrej Bauer
5 hours ago












$begingroup$
How rigid is the notion of correlation? Do you want it to act on "pure" formulas (e.g. some syntactic elements that do not contain symbols for any corelation)? Does a corelation have an arity (Goedel numbering is unary; do you have binary examples or ideas for corelations without a fixed arity)? If I saw more, I might recall something from the Universal Algebra. Since you are looking for a dual, one tactic is to hope for some form of Galois connection and look for literature involving your notion and a Galois connection. Gerhard "Or Combine With Other Ingredients" Paseman, 2019.03.18.
$endgroup$
– Gerhard Paseman
5 hours ago




$begingroup$
How rigid is the notion of correlation? Do you want it to act on "pure" formulas (e.g. some syntactic elements that do not contain symbols for any corelation)? Does a corelation have an arity (Goedel numbering is unary; do you have binary examples or ideas for corelations without a fixed arity)? If I saw more, I might recall something from the Universal Algebra. Since you are looking for a dual, one tactic is to hope for some form of Galois connection and look for literature involving your notion and a Galois connection. Gerhard "Or Combine With Other Ingredients" Paseman, 2019.03.18.
$endgroup$
– Gerhard Paseman
5 hours ago




2




2




$begingroup$
Would your co-relations include things like set-comprehension, where $x:phi(x)$ is a term produced from a formula $phi(x)$? If so, then probably you'd also include things like $lambda$-abstraction and Hilbert's $epsilon$ operator.
$endgroup$
– Andreas Blass
5 hours ago




$begingroup$
Would your co-relations include things like set-comprehension, where $x:phi(x)$ is a term produced from a formula $phi(x)$? If so, then probably you'd also include things like $lambda$-abstraction and Hilbert's $epsilon$ operator.
$endgroup$
– Andreas Blass
5 hours ago












$begingroup$
@AndrejBauer Yes please, that's more than acceptable! (And I think I'm already thinking along those lines, but laboriously and inefficiently.)
$endgroup$
– Noah Schweber
5 hours ago





$begingroup$
@AndrejBauer Yes please, that's more than acceptable! (And I think I'm already thinking along those lines, but laboriously and inefficiently.)
$endgroup$
– Noah Schweber
5 hours ago











2 Answers
2






active

oldest

votes


















5












$begingroup$

Let us first distinguish between two kinds of operations that "take formulas to terms":



  1. We might ask for reflection of syntax into the theory. A typical example is a quoting operator which takes a formula and returns its Gödel number.


  2. We might ask for the ability to mix formulas and terms. A typical example is the subset-forming operation $x in A mid phi(x)$.


The two are quite different because the first one is quite intensional (logically equivalent formulas produce different numbers) while the second one is extensional (logically equivalent formula produce the same subset).



Reflection of syntax into theory gets interesting once we ask for it to play nicely with respect to substitution and binding. I am not too familiar with this area, you could look at how syntax is reflected into NuPRL. You might also be interested in going in the other direction, namely how to convert internal representation of syntax to formulas. This goes under the name "meta-programming", where once again I am not too familiar with the literature. I am for instance aware of Aleks Nanevski's work on meta-programming with names and necessity.



For the second part (terms that contains formulas), that's very familiar territory in higher-order logic and type theory. If terms can appear in formulas and formulas can appear in terms, then the two-level stratification of terms and formulas familiar from first-order logic becomes meaningless. It is then better to put formulas and terms on equal footing and use sorts or types to keep track of what is what. One example of such a setup is Church's type theory where there is a special type of truth values. A more modern example is dependent type theory, especially variants of it that have a dedicated sort or universe of propositions, for instance the Calculus of constructions.



If you are interested to see how such formal systems work in practice, you can look at modern proof assistants. They all eschew the traditional first-order logic (because it is inappropriate for mathematical practice) and use one of the above mentioned formalisms instead: Isabelle/HOL uses Church-style higher-order logic, Coq uses the Inductive Calculus of Constructions, and Agda uses Martin-Löf type theory.






share|cite|improve this answer









$endgroup$












  • $begingroup$
    Thank you very much! The first (non-extensional) approach is what I'm interested in; I've edited to make that clear. If you don't mind, I'm going to hold off on accepting this answer for a bit, in case other answers appear.
    $endgroup$
    – Noah Schweber
    3 hours ago


















-1












$begingroup$

If I understand you correctly, you might like what Feferman and Jager call BON, the basic theory of operations and numbers, based on one of Beeson's theories. See "Systems of explicit mathematics with non-constructive $mu$ operator", APAL 65 (1993), 243-263, or here.



In this theory all the definable functions are given by terms. Functions may have partial domains, and the symbol $fxdownarrow$ indicates that $fx$ is defined. There is a term $mu$ of the form
$$mu:(N rightarrow N) rightarrow N$$
meaning "the minimum $x$ with $fx=0$, if it exists" -- and you might reasonably call this a co-relation.



The result is a theory for which, as shown in the last result of the paper:
$$BON(mu)+(FMLA!-!Ind_N)equiv P!A_Omega^w equiv widehatID_1
equiv (Pi_infty^0-CA)_<epsilon_0$$






share|cite|improve this answer









$endgroup$












  • $begingroup$
    I think this is interesting, but it's just an example - I'm looking for a general theory of such things, analogous to the basic model theory of first-order logic (that is, considering arbitrary signatures of constant, function, relation,and co-relation symbols). This doesn't seem to be that.
    $endgroup$
    – Noah Schweber
    5 hours ago










  • $begingroup$
    I've edited to make this clear.
    $endgroup$
    – Noah Schweber
    5 hours ago










  • $begingroup$
    Fair enough, I'll leave this up as an example of what a general theory might cover.
    $endgroup$
    – Matt F.
    4 hours ago










  • $begingroup$
    I would actually prefer if this were a comment, given that it doesn't address the question.
    $endgroup$
    – Noah Schweber
    3 hours ago










  • $begingroup$
    @NoahSchweber, you're welcome to write up it as a comment if you like.
    $endgroup$
    – Matt F.
    3 hours ago










Your Answer





StackExchange.ifUsing("editor", function ()
return StackExchange.using("mathjaxEditing", function ()
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix)
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
);
);
, "mathjax-editing");

StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "504"
;
initTagRenderer("".split(" "), "".split(" "), channelOptions);

StackExchange.using("externalEditor", function()
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled)
StackExchange.using("snippets", function()
createEditor();
);

else
createEditor();

);

function createEditor()
StackExchange.prepareEditor(
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader:
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
,
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);



);













draft saved

draft discarded


















StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f325706%2flogic-with-co-relations-sources%23new-answer', 'question_page');

);

Post as a guest















Required, but never shown

























2 Answers
2






active

oldest

votes








2 Answers
2






active

oldest

votes









active

oldest

votes






active

oldest

votes









5












$begingroup$

Let us first distinguish between two kinds of operations that "take formulas to terms":



  1. We might ask for reflection of syntax into the theory. A typical example is a quoting operator which takes a formula and returns its Gödel number.


  2. We might ask for the ability to mix formulas and terms. A typical example is the subset-forming operation $x in A mid phi(x)$.


The two are quite different because the first one is quite intensional (logically equivalent formulas produce different numbers) while the second one is extensional (logically equivalent formula produce the same subset).



Reflection of syntax into theory gets interesting once we ask for it to play nicely with respect to substitution and binding. I am not too familiar with this area, you could look at how syntax is reflected into NuPRL. You might also be interested in going in the other direction, namely how to convert internal representation of syntax to formulas. This goes under the name "meta-programming", where once again I am not too familiar with the literature. I am for instance aware of Aleks Nanevski's work on meta-programming with names and necessity.



For the second part (terms that contains formulas), that's very familiar territory in higher-order logic and type theory. If terms can appear in formulas and formulas can appear in terms, then the two-level stratification of terms and formulas familiar from first-order logic becomes meaningless. It is then better to put formulas and terms on equal footing and use sorts or types to keep track of what is what. One example of such a setup is Church's type theory where there is a special type of truth values. A more modern example is dependent type theory, especially variants of it that have a dedicated sort or universe of propositions, for instance the Calculus of constructions.



If you are interested to see how such formal systems work in practice, you can look at modern proof assistants. They all eschew the traditional first-order logic (because it is inappropriate for mathematical practice) and use one of the above mentioned formalisms instead: Isabelle/HOL uses Church-style higher-order logic, Coq uses the Inductive Calculus of Constructions, and Agda uses Martin-Löf type theory.






share|cite|improve this answer









$endgroup$












  • $begingroup$
    Thank you very much! The first (non-extensional) approach is what I'm interested in; I've edited to make that clear. If you don't mind, I'm going to hold off on accepting this answer for a bit, in case other answers appear.
    $endgroup$
    – Noah Schweber
    3 hours ago















5












$begingroup$

Let us first distinguish between two kinds of operations that "take formulas to terms":



  1. We might ask for reflection of syntax into the theory. A typical example is a quoting operator which takes a formula and returns its Gödel number.


  2. We might ask for the ability to mix formulas and terms. A typical example is the subset-forming operation $x in A mid phi(x)$.


The two are quite different because the first one is quite intensional (logically equivalent formulas produce different numbers) while the second one is extensional (logically equivalent formula produce the same subset).



Reflection of syntax into theory gets interesting once we ask for it to play nicely with respect to substitution and binding. I am not too familiar with this area, you could look at how syntax is reflected into NuPRL. You might also be interested in going in the other direction, namely how to convert internal representation of syntax to formulas. This goes under the name "meta-programming", where once again I am not too familiar with the literature. I am for instance aware of Aleks Nanevski's work on meta-programming with names and necessity.



For the second part (terms that contains formulas), that's very familiar territory in higher-order logic and type theory. If terms can appear in formulas and formulas can appear in terms, then the two-level stratification of terms and formulas familiar from first-order logic becomes meaningless. It is then better to put formulas and terms on equal footing and use sorts or types to keep track of what is what. One example of such a setup is Church's type theory where there is a special type of truth values. A more modern example is dependent type theory, especially variants of it that have a dedicated sort or universe of propositions, for instance the Calculus of constructions.



If you are interested to see how such formal systems work in practice, you can look at modern proof assistants. They all eschew the traditional first-order logic (because it is inappropriate for mathematical practice) and use one of the above mentioned formalisms instead: Isabelle/HOL uses Church-style higher-order logic, Coq uses the Inductive Calculus of Constructions, and Agda uses Martin-Löf type theory.






share|cite|improve this answer









$endgroup$












  • $begingroup$
    Thank you very much! The first (non-extensional) approach is what I'm interested in; I've edited to make that clear. If you don't mind, I'm going to hold off on accepting this answer for a bit, in case other answers appear.
    $endgroup$
    – Noah Schweber
    3 hours ago













5












5








5





$begingroup$

Let us first distinguish between two kinds of operations that "take formulas to terms":



  1. We might ask for reflection of syntax into the theory. A typical example is a quoting operator which takes a formula and returns its Gödel number.


  2. We might ask for the ability to mix formulas and terms. A typical example is the subset-forming operation $x in A mid phi(x)$.


The two are quite different because the first one is quite intensional (logically equivalent formulas produce different numbers) while the second one is extensional (logically equivalent formula produce the same subset).



Reflection of syntax into theory gets interesting once we ask for it to play nicely with respect to substitution and binding. I am not too familiar with this area, you could look at how syntax is reflected into NuPRL. You might also be interested in going in the other direction, namely how to convert internal representation of syntax to formulas. This goes under the name "meta-programming", where once again I am not too familiar with the literature. I am for instance aware of Aleks Nanevski's work on meta-programming with names and necessity.



For the second part (terms that contains formulas), that's very familiar territory in higher-order logic and type theory. If terms can appear in formulas and formulas can appear in terms, then the two-level stratification of terms and formulas familiar from first-order logic becomes meaningless. It is then better to put formulas and terms on equal footing and use sorts or types to keep track of what is what. One example of such a setup is Church's type theory where there is a special type of truth values. A more modern example is dependent type theory, especially variants of it that have a dedicated sort or universe of propositions, for instance the Calculus of constructions.



If you are interested to see how such formal systems work in practice, you can look at modern proof assistants. They all eschew the traditional first-order logic (because it is inappropriate for mathematical practice) and use one of the above mentioned formalisms instead: Isabelle/HOL uses Church-style higher-order logic, Coq uses the Inductive Calculus of Constructions, and Agda uses Martin-Löf type theory.






share|cite|improve this answer









$endgroup$



Let us first distinguish between two kinds of operations that "take formulas to terms":



  1. We might ask for reflection of syntax into the theory. A typical example is a quoting operator which takes a formula and returns its Gödel number.


  2. We might ask for the ability to mix formulas and terms. A typical example is the subset-forming operation $x in A mid phi(x)$.


The two are quite different because the first one is quite intensional (logically equivalent formulas produce different numbers) while the second one is extensional (logically equivalent formula produce the same subset).



Reflection of syntax into theory gets interesting once we ask for it to play nicely with respect to substitution and binding. I am not too familiar with this area, you could look at how syntax is reflected into NuPRL. You might also be interested in going in the other direction, namely how to convert internal representation of syntax to formulas. This goes under the name "meta-programming", where once again I am not too familiar with the literature. I am for instance aware of Aleks Nanevski's work on meta-programming with names and necessity.



For the second part (terms that contains formulas), that's very familiar territory in higher-order logic and type theory. If terms can appear in formulas and formulas can appear in terms, then the two-level stratification of terms and formulas familiar from first-order logic becomes meaningless. It is then better to put formulas and terms on equal footing and use sorts or types to keep track of what is what. One example of such a setup is Church's type theory where there is a special type of truth values. A more modern example is dependent type theory, especially variants of it that have a dedicated sort or universe of propositions, for instance the Calculus of constructions.



If you are interested to see how such formal systems work in practice, you can look at modern proof assistants. They all eschew the traditional first-order logic (because it is inappropriate for mathematical practice) and use one of the above mentioned formalisms instead: Isabelle/HOL uses Church-style higher-order logic, Coq uses the Inductive Calculus of Constructions, and Agda uses Martin-Löf type theory.







share|cite|improve this answer












share|cite|improve this answer



share|cite|improve this answer










answered 4 hours ago









Andrej BauerAndrej Bauer

31k480170




31k480170











  • $begingroup$
    Thank you very much! The first (non-extensional) approach is what I'm interested in; I've edited to make that clear. If you don't mind, I'm going to hold off on accepting this answer for a bit, in case other answers appear.
    $endgroup$
    – Noah Schweber
    3 hours ago
















  • $begingroup$
    Thank you very much! The first (non-extensional) approach is what I'm interested in; I've edited to make that clear. If you don't mind, I'm going to hold off on accepting this answer for a bit, in case other answers appear.
    $endgroup$
    – Noah Schweber
    3 hours ago















$begingroup$
Thank you very much! The first (non-extensional) approach is what I'm interested in; I've edited to make that clear. If you don't mind, I'm going to hold off on accepting this answer for a bit, in case other answers appear.
$endgroup$
– Noah Schweber
3 hours ago




$begingroup$
Thank you very much! The first (non-extensional) approach is what I'm interested in; I've edited to make that clear. If you don't mind, I'm going to hold off on accepting this answer for a bit, in case other answers appear.
$endgroup$
– Noah Schweber
3 hours ago











-1












$begingroup$

If I understand you correctly, you might like what Feferman and Jager call BON, the basic theory of operations and numbers, based on one of Beeson's theories. See "Systems of explicit mathematics with non-constructive $mu$ operator", APAL 65 (1993), 243-263, or here.



In this theory all the definable functions are given by terms. Functions may have partial domains, and the symbol $fxdownarrow$ indicates that $fx$ is defined. There is a term $mu$ of the form
$$mu:(N rightarrow N) rightarrow N$$
meaning "the minimum $x$ with $fx=0$, if it exists" -- and you might reasonably call this a co-relation.



The result is a theory for which, as shown in the last result of the paper:
$$BON(mu)+(FMLA!-!Ind_N)equiv P!A_Omega^w equiv widehatID_1
equiv (Pi_infty^0-CA)_<epsilon_0$$






share|cite|improve this answer









$endgroup$












  • $begingroup$
    I think this is interesting, but it's just an example - I'm looking for a general theory of such things, analogous to the basic model theory of first-order logic (that is, considering arbitrary signatures of constant, function, relation,and co-relation symbols). This doesn't seem to be that.
    $endgroup$
    – Noah Schweber
    5 hours ago










  • $begingroup$
    I've edited to make this clear.
    $endgroup$
    – Noah Schweber
    5 hours ago










  • $begingroup$
    Fair enough, I'll leave this up as an example of what a general theory might cover.
    $endgroup$
    – Matt F.
    4 hours ago










  • $begingroup$
    I would actually prefer if this were a comment, given that it doesn't address the question.
    $endgroup$
    – Noah Schweber
    3 hours ago










  • $begingroup$
    @NoahSchweber, you're welcome to write up it as a comment if you like.
    $endgroup$
    – Matt F.
    3 hours ago















-1












$begingroup$

If I understand you correctly, you might like what Feferman and Jager call BON, the basic theory of operations and numbers, based on one of Beeson's theories. See "Systems of explicit mathematics with non-constructive $mu$ operator", APAL 65 (1993), 243-263, or here.



In this theory all the definable functions are given by terms. Functions may have partial domains, and the symbol $fxdownarrow$ indicates that $fx$ is defined. There is a term $mu$ of the form
$$mu:(N rightarrow N) rightarrow N$$
meaning "the minimum $x$ with $fx=0$, if it exists" -- and you might reasonably call this a co-relation.



The result is a theory for which, as shown in the last result of the paper:
$$BON(mu)+(FMLA!-!Ind_N)equiv P!A_Omega^w equiv widehatID_1
equiv (Pi_infty^0-CA)_<epsilon_0$$






share|cite|improve this answer









$endgroup$












  • $begingroup$
    I think this is interesting, but it's just an example - I'm looking for a general theory of such things, analogous to the basic model theory of first-order logic (that is, considering arbitrary signatures of constant, function, relation,and co-relation symbols). This doesn't seem to be that.
    $endgroup$
    – Noah Schweber
    5 hours ago










  • $begingroup$
    I've edited to make this clear.
    $endgroup$
    – Noah Schweber
    5 hours ago










  • $begingroup$
    Fair enough, I'll leave this up as an example of what a general theory might cover.
    $endgroup$
    – Matt F.
    4 hours ago










  • $begingroup$
    I would actually prefer if this were a comment, given that it doesn't address the question.
    $endgroup$
    – Noah Schweber
    3 hours ago










  • $begingroup$
    @NoahSchweber, you're welcome to write up it as a comment if you like.
    $endgroup$
    – Matt F.
    3 hours ago













-1












-1








-1





$begingroup$

If I understand you correctly, you might like what Feferman and Jager call BON, the basic theory of operations and numbers, based on one of Beeson's theories. See "Systems of explicit mathematics with non-constructive $mu$ operator", APAL 65 (1993), 243-263, or here.



In this theory all the definable functions are given by terms. Functions may have partial domains, and the symbol $fxdownarrow$ indicates that $fx$ is defined. There is a term $mu$ of the form
$$mu:(N rightarrow N) rightarrow N$$
meaning "the minimum $x$ with $fx=0$, if it exists" -- and you might reasonably call this a co-relation.



The result is a theory for which, as shown in the last result of the paper:
$$BON(mu)+(FMLA!-!Ind_N)equiv P!A_Omega^w equiv widehatID_1
equiv (Pi_infty^0-CA)_<epsilon_0$$






share|cite|improve this answer









$endgroup$



If I understand you correctly, you might like what Feferman and Jager call BON, the basic theory of operations and numbers, based on one of Beeson's theories. See "Systems of explicit mathematics with non-constructive $mu$ operator", APAL 65 (1993), 243-263, or here.



In this theory all the definable functions are given by terms. Functions may have partial domains, and the symbol $fxdownarrow$ indicates that $fx$ is defined. There is a term $mu$ of the form
$$mu:(N rightarrow N) rightarrow N$$
meaning "the minimum $x$ with $fx=0$, if it exists" -- and you might reasonably call this a co-relation.



The result is a theory for which, as shown in the last result of the paper:
$$BON(mu)+(FMLA!-!Ind_N)equiv P!A_Omega^w equiv widehatID_1
equiv (Pi_infty^0-CA)_<epsilon_0$$







share|cite|improve this answer












share|cite|improve this answer



share|cite|improve this answer










answered 5 hours ago









Matt F.Matt F.

6,80911746




6,80911746











  • $begingroup$
    I think this is interesting, but it's just an example - I'm looking for a general theory of such things, analogous to the basic model theory of first-order logic (that is, considering arbitrary signatures of constant, function, relation,and co-relation symbols). This doesn't seem to be that.
    $endgroup$
    – Noah Schweber
    5 hours ago










  • $begingroup$
    I've edited to make this clear.
    $endgroup$
    – Noah Schweber
    5 hours ago










  • $begingroup$
    Fair enough, I'll leave this up as an example of what a general theory might cover.
    $endgroup$
    – Matt F.
    4 hours ago










  • $begingroup$
    I would actually prefer if this were a comment, given that it doesn't address the question.
    $endgroup$
    – Noah Schweber
    3 hours ago










  • $begingroup$
    @NoahSchweber, you're welcome to write up it as a comment if you like.
    $endgroup$
    – Matt F.
    3 hours ago
















  • $begingroup$
    I think this is interesting, but it's just an example - I'm looking for a general theory of such things, analogous to the basic model theory of first-order logic (that is, considering arbitrary signatures of constant, function, relation,and co-relation symbols). This doesn't seem to be that.
    $endgroup$
    – Noah Schweber
    5 hours ago










  • $begingroup$
    I've edited to make this clear.
    $endgroup$
    – Noah Schweber
    5 hours ago










  • $begingroup$
    Fair enough, I'll leave this up as an example of what a general theory might cover.
    $endgroup$
    – Matt F.
    4 hours ago










  • $begingroup$
    I would actually prefer if this were a comment, given that it doesn't address the question.
    $endgroup$
    – Noah Schweber
    3 hours ago










  • $begingroup$
    @NoahSchweber, you're welcome to write up it as a comment if you like.
    $endgroup$
    – Matt F.
    3 hours ago















$begingroup$
I think this is interesting, but it's just an example - I'm looking for a general theory of such things, analogous to the basic model theory of first-order logic (that is, considering arbitrary signatures of constant, function, relation,and co-relation symbols). This doesn't seem to be that.
$endgroup$
– Noah Schweber
5 hours ago




$begingroup$
I think this is interesting, but it's just an example - I'm looking for a general theory of such things, analogous to the basic model theory of first-order logic (that is, considering arbitrary signatures of constant, function, relation,and co-relation symbols). This doesn't seem to be that.
$endgroup$
– Noah Schweber
5 hours ago












$begingroup$
I've edited to make this clear.
$endgroup$
– Noah Schweber
5 hours ago




$begingroup$
I've edited to make this clear.
$endgroup$
– Noah Schweber
5 hours ago












$begingroup$
Fair enough, I'll leave this up as an example of what a general theory might cover.
$endgroup$
– Matt F.
4 hours ago




$begingroup$
Fair enough, I'll leave this up as an example of what a general theory might cover.
$endgroup$
– Matt F.
4 hours ago












$begingroup$
I would actually prefer if this were a comment, given that it doesn't address the question.
$endgroup$
– Noah Schweber
3 hours ago




$begingroup$
I would actually prefer if this were a comment, given that it doesn't address the question.
$endgroup$
– Noah Schweber
3 hours ago












$begingroup$
@NoahSchweber, you're welcome to write up it as a comment if you like.
$endgroup$
– Matt F.
3 hours ago




$begingroup$
@NoahSchweber, you're welcome to write up it as a comment if you like.
$endgroup$
– Matt F.
3 hours ago

















draft saved

draft discarded
















































Thanks for contributing an answer to MathOverflow!


  • Please be sure to answer the question. Provide details and share your research!

But avoid


  • Asking for help, clarification, or responding to other answers.

  • Making statements based on opinion; back them up with references or personal experience.

Use MathJax to format equations. MathJax reference.


To learn more, see our tips on writing great answers.




draft saved


draft discarded














StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f325706%2flogic-with-co-relations-sources%23new-answer', 'question_page');

);

Post as a guest















Required, but never shown





















































Required, but never shown














Required, but never shown












Required, but never shown







Required, but never shown

































Required, but never shown














Required, but never shown












Required, but never shown







Required, but never shown







Popular posts from this blog

名間水力發電廠 目录 沿革 設施 鄰近設施 註釋 外部連結 导航菜单23°50′10″N 120°42′41″E / 23.83611°N 120.71139°E / 23.83611; 120.7113923°50′10″N 120°42′41″E / 23.83611°N 120.71139°E / 23.83611; 120.71139計畫概要原始内容臺灣第一座BOT 模式開發的水力發電廠-名間水力電廠名間水力發電廠 水利署首件BOT案原始内容《小檔案》名間電廠 首座BOT水力發電廠原始内容名間電廠BOT - 經濟部水利署中區水資源局

Prove that NP is closed under karp reduction?Space(n) not closed under Karp reductions - what about NTime(n)?Class P is closed under rotation?Prove or disprove that $NL$ is closed under polynomial many-one reductions$mathbfNC_2$ is closed under log-space reductionOn Karp reductionwhen can I know if a class (complexity) is closed under reduction (cook/karp)Check if class $PSPACE$ is closed under polyonomially space reductionIs NPSPACE also closed under polynomial-time reduction and under log-space reduction?Prove PSPACE is closed under complement?Prove PSPACE is closed under union?

Is my guitar’s action too high? Announcing the arrival of Valued Associate #679: Cesar Manara Planned maintenance scheduled April 23, 2019 at 23:30 UTC (7:30pm US/Eastern)Strings too stiff on a recently purchased acoustic guitar | Cort AD880CEIs the action of my guitar really high?Μy little finger is too weak to play guitarWith guitar, how long should I give my fingers to strengthen / callous?When playing a fret the guitar sounds mutedPlaying (Barre) chords up the guitar neckI think my guitar strings are wound too tight and I can't play barre chordsF barre chord on an SG guitarHow to find to the right strings of a barre chord by feel?High action on higher fret on my steel acoustic guitar