Mixing
Axiom checking as type checking?
$begingroup$
There is a connection between type theory and logic, where types are propositions, and type checking performs the role of checking whether a proof of a proposition is correct (Curry-Howard isomorphism).
But I can imagine a different connection: There seems to be a similarity between type checking and checking whether a particular mathematical structure satisfies a set of axioms.
We might say that propositions (axioms) are formalized as types (just as in the CH-isomorphism), but that now, an instance of a proposition (i.e. an instance of that type) is not a proof of the proposition, but a model of it. Type checking then takes the role of checking whether a particular mathematical structure is indeed a model of that axiom.
Is there a formalization of "checking whether a structure is a model of a proposition" as type checking? Could you explain such a formalization, or point to an explanation of it?
logic model-theory axioms type-theory
asked Jan 31 at 18:58
user56834user56834
3,29021253
$endgroup$
add a comment |
$begingroup$
There is a connection between type theory and logic, where types are propositions, and type checking performs the role of checking whether a proof of a proposition is correct (Curry-Howard isomorphism).
But I can imagine a different connection: There seems to be a similarity between type checking and checking whether a particular mathematical structure satisfies a set of axioms.
We might say that propositions (axioms) are formalized as types (just as in the CH-isomorphism), but that now, an instance of a proposition (i.e. an instance of that type) is not a proof of the proposition, but a model of it. Type checking then takes the role of checking whether a particular mathematical structure is indeed a model of that axiom.
Is there a formalization of "checking whether a structure is a model of a proposition" as type checking? Could you explain such a formalization, or point to an explanation of it?
logic model-theory axioms type-theory
asked Jan 31 at 18:58
user56834user56834
3,29021253
$endgroup$
$begingroup$
Related question: math.stackexchange.com/questions/1697288/…
$endgroup$
– user56834
Mar 25 at 12:23
add a comment |
$begingroup$
There is a connection between type theory and logic, where types are propositions, and type checking performs the role of checking whether a proof of a proposition is correct (Curry-Howard isomorphism).
But I can imagine a different connection: There seems to be a similarity between type checking and checking whether a particular mathematical structure satisfies a set of axioms.
We might say that propositions (axioms) are formalized as types (just as in the CH-isomorphism), but that now, an instance of a proposition (i.e. an instance of that type) is not a proof of the proposition, but a model of it. Type checking then takes the role of checking whether a particular mathematical structure is indeed a model of that axiom.
Is there a formalization of "checking whether a structure is a model of a proposition" as type checking? Could you explain such a formalization, or point to an explanation of it?
logic model-theory axioms type-theory
asked Jan 31 at 18:58
user56834user56834
3,29021253
$endgroup$
There is a connection between type theory and logic, where types are propositions, and type checking performs the role of checking whether a proof of a proposition is correct (Curry-Howard isomorphism).
But I can imagine a different connection: There seems to be a similarity between type checking and checking whether a particular mathematical structure satisfies a set of axioms.
We might say that propositions (axioms) are formalized as types (just as in the CH-isomorphism), but that now, an instance of a proposition (i.e. an instance of that type) is not a proof of the proposition, but a model of it. Type checking then takes the role of checking whether a particular mathematical structure is indeed a model of that axiom.
Is there a formalization of "checking whether a structure is a model of a proposition" as type checking? Could you explain such a formalization, or point to an explanation of it?
logic model-theory axioms type-theory
logic model-theory axioms type-theory
asked Jan 31 at 18:58
user56834user56834
3,29021253
asked Jan 31 at 18:58
user56834user56834
3,29021253
edited Feb 7 at 12:03
user56834
asked Jan 31 at 18:58
user56834user56834
3,29021253
asked Jan 31 at 18:58
user56834user56834
3,29021253
asked Jan 31 at 18:58
user56834user56834
3,29021253
3,29021253
$begingroup$
Related question: math.stackexchange.com/questions/1697288/…
$endgroup$
– user56834
Mar 25 at 12:23
add a comment |
$begingroup$
Related question: math.stackexchange.com/questions/1697288/…
$endgroup$
– user56834
Mar 25 at 12:23
$begingroup$
Related question: math.stackexchange.com/questions/1697288/…
$endgroup$
– user56834
Mar 25 at 12:23
$begingroup$
Related question: math.stackexchange.com/questions/1697288/…
$endgroup$
– user56834
Mar 25 at 12:23
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
The key observation of the Curry-Howard correspondence is that the inductive structure of terms in type theory mirrors the inductive structure of proofs in logic.
For example, given two terms $t_1$ and $t_2$ of types $A_1$ and $A_2$, I can construct a term $(t_1,t_2)$ of the product type $A_1times A_2$. Similarly, given two proofs $p_1$ and $p_2$ of the propositions $Q_1$ and $Q_2$, I can put them together to form a proof $(p_1,p_2)$ of the conjunction $Q_1land Q_2$.
On the other hand, models of a proposition (at least in ordinary semantics for first-order / predicate logic) just don't have this same kind of inductive structure. Given models $M_1$ and $M_2$ of sentences $varphi_1$ and $varphi_2$, there's no canonical way of constructing a model of the conjunction $varphi_1land varphi_2$. So I'm not optimistic that the kind of extension of Curry-Howard that you're looking for is possible.
It's conceivable to me that you could change the notion of "model" to something sufficiently syntactic to make this work - but that would likely involve making a "model" of $varphi$ essentially an encoding of a proof of $varphi$, and then relying on the usual Curry-Howard correspondence.
answered Feb 4 at 15:48
Alex KruckmanAlex Kruckman
28.5k32758
$endgroup$
$begingroup$
very interesting
$endgroup$
– user56834
Feb 4 at 15:56
$begingroup$
Could you elaborate a bit more? e.g. make intuitively more clear why models don't have an "inductive structure", and what this means for why we probably can't use type theory?
$endgroup$
– user56834
Feb 7 at 18:27
$begingroup$
I'm asking that because I think your point is interesting and I'd like to understand it better
$endgroup$
– user56834
Feb 9 at 6:00
add a comment |
$begingroup$
Yes, there are two notions of "fit into" here:
- Terms (what you call instances here) "fit into" types or don't, and that is checked when you do type checking
- Structures (e.g. set theoretical constructions) "fit into" propositions or don't, and that's checked by when you verify whether the structure is a model.
I think there's nothing wrong with drawing an analogy of how things "fit into" another here, as both processes can be considered under the guise of a computational task. Although there are many stratification involved.
- For one, mathematical logicans (and e.g. set theorists) will do everything formalistically with symbols on paper, but nontheless they make a conceptual distrinction between syntax and semantics. As a result, you have philosophical positions like mathematical Platonism which consider mathematical structures as farther away from syntax and closer to something "actual". Something that's realized among possible semantics. Computer science type theorists (which are also logicans of course, just sometimes closer to another school, say the proof theorist ones) will work in large parts purely on the syntactic side (and semantics are sought in more general setups than e.g. in set theorists departments)
- Secondly, as mentioned, both "checkings" here are forms of computations and it's worth pointing out that what's doable here will depend on the underlying logic. The Hindley–Milner type system is the framework that motivated the programming languages ML and then Haskell, and grants a nice type checking routine. The frameworks where good checking is possible made cuts. Modern efforts in ramping up a dependently typed language gear towards a constructive/intuitionistic logic that now include strong forms of quantifiers, while logicans and model theorists do large parts do a deeper and thus less varied (relatively speaking) study of the long established strong first- or higher order logics. The answers in this logic SE questions are one among the most interesting on the platform. As is always the case with such broad questions on logic, one could now go down many rabbit holds. I might give a shoutout to Tarski's restricting theorem for strong logics. Decidability is also a question for type systems, if you just choose any.
- Along with the theme of restrictions, type checking of a term checks all it can, while with propositions, there's always many and different aspects of a structure you can validate. Again, here, if you make cuts and your type system admits subtyping and whatnot, I suppose you can take coarser views on terms here too.
- In the latter notion of "fit in", there's the concept of categoricity and one may try to reflect that in uniqueness types.
- If you have narrowed down a your logics of interest and decide you want to approach your question from a raw computation and "fit into" perspective, then the subject of abstract rewriting and rewriting systems, which may strike one as even more formal than subfields mathematical logic, may be down your alley.
Side note 1: The verification process in the latter case need not even be restricted to axioms but we can do that for any propositions.
Side note 2: I'm not a fan of your initial wording "checking whether a proof of a proposition is correct". I'd instead say "checking whether an expression is a proof of a proposition". I say that because if you use your language here, then we grant every term the status of being a "wrong proof" for almost all propositions. That's just a question of our language here, though.
edited Feb 9 at 6:21
user56834
3,29021253
answered Feb 3 at 11:03
Nikolaj-KNikolaj-K
5,96723069
$endgroup$
1
$begingroup$
@user56834 That's a very dry and concise response for me giving you various pointers. Let me not take offense here and just reiterate that I think the two notions are captured by the task to evaluate a yes-or-no valued algorithm, and with type systems that algorithms comes with that system and with a general logic it might not exist at all. I'm not aware of work that explicitly tries to join those challanges.
$endgroup$
– Nikolaj-K
Feb 3 at 15:38
$begingroup$
I re-read it, and I admit I was being uncharitable. My apologies.
$endgroup$
– user56834
Feb 9 at 6:21
$begingroup$
What do you think of Alex Kruckman's answer?
$endgroup$
– user56834
Feb 9 at 6:22
add a comment |
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: "69"
};
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
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3095310%2faxiom-checking-as-type-checking%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
$begingroup$
The key observation of the Curry-Howard correspondence is that the inductive structure of terms in type theory mirrors the inductive structure of proofs in logic.
For example, given two terms $t_1$ and $t_2$ of types $A_1$ and $A_2$, I can construct a term $(t_1,t_2)$ of the product type $A_1times A_2$. Similarly, given two proofs $p_1$ and $p_2$ of the propositions $Q_1$ and $Q_2$, I can put them together to form a proof $(p_1,p_2)$ of the conjunction $Q_1land Q_2$.
On the other hand, models of a proposition (at least in ordinary semantics for first-order / predicate logic) just don't have this same kind of inductive structure. Given models $M_1$ and $M_2$ of sentences $varphi_1$ and $varphi_2$, there's no canonical way of constructing a model of the conjunction $varphi_1land varphi_2$. So I'm not optimistic that the kind of extension of Curry-Howard that you're looking for is possible.
It's conceivable to me that you could change the notion of "model" to something sufficiently syntactic to make this work - but that would likely involve making a "model" of $varphi$ essentially an encoding of a proof of $varphi$, and then relying on the usual Curry-Howard correspondence.
answered Feb 4 at 15:48
Alex KruckmanAlex Kruckman
28.5k32758
$endgroup$
$begingroup$
very interesting
$endgroup$
– user56834
Feb 4 at 15:56
$begingroup$
Could you elaborate a bit more? e.g. make intuitively more clear why models don't have an "inductive structure", and what this means for why we probably can't use type theory?
$endgroup$
– user56834
Feb 7 at 18:27
$begingroup$
I'm asking that because I think your point is interesting and I'd like to understand it better
$endgroup$
– user56834
Feb 9 at 6:00
add a comment |
$begingroup$
The key observation of the Curry-Howard correspondence is that the inductive structure of terms in type theory mirrors the inductive structure of proofs in logic.
For example, given two terms $t_1$ and $t_2$ of types $A_1$ and $A_2$, I can construct a term $(t_1,t_2)$ of the product type $A_1times A_2$. Similarly, given two proofs $p_1$ and $p_2$ of the propositions $Q_1$ and $Q_2$, I can put them together to form a proof $(p_1,p_2)$ of the conjunction $Q_1land Q_2$.
On the other hand, models of a proposition (at least in ordinary semantics for first-order / predicate logic) just don't have this same kind of inductive structure. Given models $M_1$ and $M_2$ of sentences $varphi_1$ and $varphi_2$, there's no canonical way of constructing a model of the conjunction $varphi_1land varphi_2$. So I'm not optimistic that the kind of extension of Curry-Howard that you're looking for is possible.
It's conceivable to me that you could change the notion of "model" to something sufficiently syntactic to make this work - but that would likely involve making a "model" of $varphi$ essentially an encoding of a proof of $varphi$, and then relying on the usual Curry-Howard correspondence.
answered Feb 4 at 15:48
Alex KruckmanAlex Kruckman
28.5k32758
$endgroup$
$begingroup$
very interesting
$endgroup$
– user56834
Feb 4 at 15:56
$begingroup$
Could you elaborate a bit more? e.g. make intuitively more clear why models don't have an "inductive structure", and what this means for why we probably can't use type theory?
$endgroup$
– user56834
Feb 7 at 18:27
$begingroup$
I'm asking that because I think your point is interesting and I'd like to understand it better
$endgroup$
– user56834
Feb 9 at 6:00
add a comment |
$begingroup$
The key observation of the Curry-Howard correspondence is that the inductive structure of terms in type theory mirrors the inductive structure of proofs in logic.
For example, given two terms $t_1$ and $t_2$ of types $A_1$ and $A_2$, I can construct a term $(t_1,t_2)$ of the product type $A_1times A_2$. Similarly, given two proofs $p_1$ and $p_2$ of the propositions $Q_1$ and $Q_2$, I can put them together to form a proof $(p_1,p_2)$ of the conjunction $Q_1land Q_2$.
On the other hand, models of a proposition (at least in ordinary semantics for first-order / predicate logic) just don't have this same kind of inductive structure. Given models $M_1$ and $M_2$ of sentences $varphi_1$ and $varphi_2$, there's no canonical way of constructing a model of the conjunction $varphi_1land varphi_2$. So I'm not optimistic that the kind of extension of Curry-Howard that you're looking for is possible.
It's conceivable to me that you could change the notion of "model" to something sufficiently syntactic to make this work - but that would likely involve making a "model" of $varphi$ essentially an encoding of a proof of $varphi$, and then relying on the usual Curry-Howard correspondence.
answered Feb 4 at 15:48
Alex KruckmanAlex Kruckman
28.5k32758
$endgroup$
The key observation of the Curry-Howard correspondence is that the inductive structure of terms in type theory mirrors the inductive structure of proofs in logic.
For example, given two terms $t_1$ and $t_2$ of types $A_1$ and $A_2$, I can construct a term $(t_1,t_2)$ of the product type $A_1times A_2$. Similarly, given two proofs $p_1$ and $p_2$ of the propositions $Q_1$ and $Q_2$, I can put them together to form a proof $(p_1,p_2)$ of the conjunction $Q_1land Q_2$.
On the other hand, models of a proposition (at least in ordinary semantics for first-order / predicate logic) just don't have this same kind of inductive structure. Given models $M_1$ and $M_2$ of sentences $varphi_1$ and $varphi_2$, there's no canonical way of constructing a model of the conjunction $varphi_1land varphi_2$. So I'm not optimistic that the kind of extension of Curry-Howard that you're looking for is possible.
It's conceivable to me that you could change the notion of "model" to something sufficiently syntactic to make this work - but that would likely involve making a "model" of $varphi$ essentially an encoding of a proof of $varphi$, and then relying on the usual Curry-Howard correspondence.
answered Feb 4 at 15:48
Alex KruckmanAlex Kruckman
28.5k32758
answered Feb 4 at 15:48
Alex KruckmanAlex Kruckman
28.5k32758
answered Feb 4 at 15:48
Alex KruckmanAlex Kruckman
28.5k32758
answered Feb 4 at 15:48
Alex KruckmanAlex Kruckman
28.5k32758
28.5k32758
$begingroup$
very interesting
$endgroup$
– user56834
Feb 4 at 15:56
$begingroup$
Could you elaborate a bit more? e.g. make intuitively more clear why models don't have an "inductive structure", and what this means for why we probably can't use type theory?
$endgroup$
– user56834
Feb 7 at 18:27
$begingroup$
I'm asking that because I think your point is interesting and I'd like to understand it better
$endgroup$
– user56834
Feb 9 at 6:00
add a comment |
$begingroup$
very interesting
$endgroup$
– user56834
Feb 4 at 15:56
$begingroup$
Could you elaborate a bit more? e.g. make intuitively more clear why models don't have an "inductive structure", and what this means for why we probably can't use type theory?
$endgroup$
– user56834
Feb 7 at 18:27
$begingroup$
I'm asking that because I think your point is interesting and I'd like to understand it better
$endgroup$
– user56834
Feb 9 at 6:00
$begingroup$
very interesting
$endgroup$
– user56834
Feb 4 at 15:56
$begingroup$
very interesting
$endgroup$
– user56834
Feb 4 at 15:56
$begingroup$
Could you elaborate a bit more? e.g. make intuitively more clear why models don't have an "inductive structure", and what this means for why we probably can't use type theory?
$endgroup$
– user56834
Feb 7 at 18:27
$begingroup$
Could you elaborate a bit more? e.g. make intuitively more clear why models don't have an "inductive structure", and what this means for why we probably can't use type theory?
$endgroup$
– user56834
Feb 7 at 18:27
$begingroup$
I'm asking that because I think your point is interesting and I'd like to understand it better
$endgroup$
– user56834
Feb 9 at 6:00
$begingroup$
I'm asking that because I think your point is interesting and I'd like to understand it better
$endgroup$
– user56834
Feb 9 at 6:00
add a comment |
$begingroup$
Yes, there are two notions of "fit into" here:
- Terms (what you call instances here) "fit into" types or don't, and that is checked when you do type checking
- Structures (e.g. set theoretical constructions) "fit into" propositions or don't, and that's checked by when you verify whether the structure is a model.
I think there's nothing wrong with drawing an analogy of how things "fit into" another here, as both processes can be considered under the guise of a computational task. Although there are many stratification involved.
- For one, mathematical logicans (and e.g. set theorists) will do everything formalistically with symbols on paper, but nontheless they make a conceptual distrinction between syntax and semantics. As a result, you have philosophical positions like mathematical Platonism which consider mathematical structures as farther away from syntax and closer to something "actual". Something that's realized among possible semantics. Computer science type theorists (which are also logicans of course, just sometimes closer to another school, say the proof theorist ones) will work in large parts purely on the syntactic side (and semantics are sought in more general setups than e.g. in set theorists departments)
- Secondly, as mentioned, both "checkings" here are forms of computations and it's worth pointing out that what's doable here will depend on the underlying logic. The Hindley–Milner type system is the framework that motivated the programming languages ML and then Haskell, and grants a nice type checking routine. The frameworks where good checking is possible made cuts. Modern efforts in ramping up a dependently typed language gear towards a constructive/intuitionistic logic that now include strong forms of quantifiers, while logicans and model theorists do large parts do a deeper and thus less varied (relatively speaking) study of the long established strong first- or higher order logics. The answers in this logic SE questions are one among the most interesting on the platform. As is always the case with such broad questions on logic, one could now go down many rabbit holds. I might give a shoutout to Tarski's restricting theorem for strong logics. Decidability is also a question for type systems, if you just choose any.
- Along with the theme of restrictions, type checking of a term checks all it can, while with propositions, there's always many and different aspects of a structure you can validate. Again, here, if you make cuts and your type system admits subtyping and whatnot, I suppose you can take coarser views on terms here too.
- In the latter notion of "fit in", there's the concept of categoricity and one may try to reflect that in uniqueness types.
- If you have narrowed down a your logics of interest and decide you want to approach your question from a raw computation and "fit into" perspective, then the subject of abstract rewriting and rewriting systems, which may strike one as even more formal than subfields mathematical logic, may be down your alley.
Side note 1: The verification process in the latter case need not even be restricted to axioms but we can do that for any propositions.
Side note 2: I'm not a fan of your initial wording "checking whether a proof of a proposition is correct". I'd instead say "checking whether an expression is a proof of a proposition". I say that because if you use your language here, then we grant every term the status of being a "wrong proof" for almost all propositions. That's just a question of our language here, though.
edited Feb 9 at 6:21
user56834
3,29021253
answered Feb 3 at 11:03
Nikolaj-KNikolaj-K
5,96723069
$endgroup$
1
$begingroup$
@user56834 That's a very dry and concise response for me giving you various pointers. Let me not take offense here and just reiterate that I think the two notions are captured by the task to evaluate a yes-or-no valued algorithm, and with type systems that algorithms comes with that system and with a general logic it might not exist at all. I'm not aware of work that explicitly tries to join those challanges.
$endgroup$
– Nikolaj-K
Feb 3 at 15:38
$begingroup$
I re-read it, and I admit I was being uncharitable. My apologies.
$endgroup$
– user56834
Feb 9 at 6:21
$begingroup$
What do you think of Alex Kruckman's answer?
$endgroup$
– user56834
Feb 9 at 6:22
add a comment |
$begingroup$
Yes, there are two notions of "fit into" here:
- Terms (what you call instances here) "fit into" types or don't, and that is checked when you do type checking
- Structures (e.g. set theoretical constructions) "fit into" propositions or don't, and that's checked by when you verify whether the structure is a model.
I think there's nothing wrong with drawing an analogy of how things "fit into" another here, as both processes can be considered under the guise of a computational task. Although there are many stratification involved.
- For one, mathematical logicans (and e.g. set theorists) will do everything formalistically with symbols on paper, but nontheless they make a conceptual distrinction between syntax and semantics. As a result, you have philosophical positions like mathematical Platonism which consider mathematical structures as farther away from syntax and closer to something "actual". Something that's realized among possible semantics. Computer science type theorists (which are also logicans of course, just sometimes closer to another school, say the proof theorist ones) will work in large parts purely on the syntactic side (and semantics are sought in more general setups than e.g. in set theorists departments)
- Secondly, as mentioned, both "checkings" here are forms of computations and it's worth pointing out that what's doable here will depend on the underlying logic. The Hindley–Milner type system is the framework that motivated the programming languages ML and then Haskell, and grants a nice type checking routine. The frameworks where good checking is possible made cuts. Modern efforts in ramping up a dependently typed language gear towards a constructive/intuitionistic logic that now include strong forms of quantifiers, while logicans and model theorists do large parts do a deeper and thus less varied (relatively speaking) study of the long established strong first- or higher order logics. The answers in this logic SE questions are one among the most interesting on the platform. As is always the case with such broad questions on logic, one could now go down many rabbit holds. I might give a shoutout to Tarski's restricting theorem for strong logics. Decidability is also a question for type systems, if you just choose any.
- Along with the theme of restrictions, type checking of a term checks all it can, while with propositions, there's always many and different aspects of a structure you can validate. Again, here, if you make cuts and your type system admits subtyping and whatnot, I suppose you can take coarser views on terms here too.
- In the latter notion of "fit in", there's the concept of categoricity and one may try to reflect that in uniqueness types.
- If you have narrowed down a your logics of interest and decide you want to approach your question from a raw computation and "fit into" perspective, then the subject of abstract rewriting and rewriting systems, which may strike one as even more formal than subfields mathematical logic, may be down your alley.
Side note 1: The verification process in the latter case need not even be restricted to axioms but we can do that for any propositions.
Side note 2: I'm not a fan of your initial wording "checking whether a proof of a proposition is correct". I'd instead say "checking whether an expression is a proof of a proposition". I say that because if you use your language here, then we grant every term the status of being a "wrong proof" for almost all propositions. That's just a question of our language here, though.
edited Feb 9 at 6:21
user56834
3,29021253
answered Feb 3 at 11:03
Nikolaj-KNikolaj-K
5,96723069
$endgroup$
1
$begingroup$
@user56834 That's a very dry and concise response for me giving you various pointers. Let me not take offense here and just reiterate that I think the two notions are captured by the task to evaluate a yes-or-no valued algorithm, and with type systems that algorithms comes with that system and with a general logic it might not exist at all. I'm not aware of work that explicitly tries to join those challanges.
$endgroup$
– Nikolaj-K
Feb 3 at 15:38
$begingroup$
I re-read it, and I admit I was being uncharitable. My apologies.
$endgroup$
– user56834
Feb 9 at 6:21
$begingroup$
What do you think of Alex Kruckman's answer?
$endgroup$
– user56834
Feb 9 at 6:22
add a comment |
$begingroup$
Yes, there are two notions of "fit into" here:
- Terms (what you call instances here) "fit into" types or don't, and that is checked when you do type checking
- Structures (e.g. set theoretical constructions) "fit into" propositions or don't, and that's checked by when you verify whether the structure is a model.
I think there's nothing wrong with drawing an analogy of how things "fit into" another here, as both processes can be considered under the guise of a computational task. Although there are many stratification involved.
- For one, mathematical logicans (and e.g. set theorists) will do everything formalistically with symbols on paper, but nontheless they make a conceptual distrinction between syntax and semantics. As a result, you have philosophical positions like mathematical Platonism which consider mathematical structures as farther away from syntax and closer to something "actual". Something that's realized among possible semantics. Computer science type theorists (which are also logicans of course, just sometimes closer to another school, say the proof theorist ones) will work in large parts purely on the syntactic side (and semantics are sought in more general setups than e.g. in set theorists departments)
- Secondly, as mentioned, both "checkings" here are forms of computations and it's worth pointing out that what's doable here will depend on the underlying logic. The Hindley–Milner type system is the framework that motivated the programming languages ML and then Haskell, and grants a nice type checking routine. The frameworks where good checking is possible made cuts. Modern efforts in ramping up a dependently typed language gear towards a constructive/intuitionistic logic that now include strong forms of quantifiers, while logicans and model theorists do large parts do a deeper and thus less varied (relatively speaking) study of the long established strong first- or higher order logics. The answers in this logic SE questions are one among the most interesting on the platform. As is always the case with such broad questions on logic, one could now go down many rabbit holds. I might give a shoutout to Tarski's restricting theorem for strong logics. Decidability is also a question for type systems, if you just choose any.
- Along with the theme of restrictions, type checking of a term checks all it can, while with propositions, there's always many and different aspects of a structure you can validate. Again, here, if you make cuts and your type system admits subtyping and whatnot, I suppose you can take coarser views on terms here too.
- In the latter notion of "fit in", there's the concept of categoricity and one may try to reflect that in uniqueness types.
- If you have narrowed down a your logics of interest and decide you want to approach your question from a raw computation and "fit into" perspective, then the subject of abstract rewriting and rewriting systems, which may strike one as even more formal than subfields mathematical logic, may be down your alley.
Side note 1: The verification process in the latter case need not even be restricted to axioms but we can do that for any propositions.
Side note 2: I'm not a fan of your initial wording "checking whether a proof of a proposition is correct". I'd instead say "checking whether an expression is a proof of a proposition". I say that because if you use your language here, then we grant every term the status of being a "wrong proof" for almost all propositions. That's just a question of our language here, though.
edited Feb 9 at 6:21
user56834
3,29021253
answered Feb 3 at 11:03
Nikolaj-KNikolaj-K
5,96723069
$endgroup$
Yes, there are two notions of "fit into" here:
- Terms (what you call instances here) "fit into" types or don't, and that is checked when you do type checking
- Structures (e.g. set theoretical constructions) "fit into" propositions or don't, and that's checked by when you verify whether the structure is a model.
I think there's nothing wrong with drawing an analogy of how things "fit into" another here, as both processes can be considered under the guise of a computational task. Although there are many stratification involved.
- For one, mathematical logicans (and e.g. set theorists) will do everything formalistically with symbols on paper, but nontheless they make a conceptual distrinction between syntax and semantics. As a result, you have philosophical positions like mathematical Platonism which consider mathematical structures as farther away from syntax and closer to something "actual". Something that's realized among possible semantics. Computer science type theorists (which are also logicans of course, just sometimes closer to another school, say the proof theorist ones) will work in large parts purely on the syntactic side (and semantics are sought in more general setups than e.g. in set theorists departments)
- Secondly, as mentioned, both "checkings" here are forms of computations and it's worth pointing out that what's doable here will depend on the underlying logic. The Hindley–Milner type system is the framework that motivated the programming languages ML and then Haskell, and grants a nice type checking routine. The frameworks where good checking is possible made cuts. Modern efforts in ramping up a dependently typed language gear towards a constructive/intuitionistic logic that now include strong forms of quantifiers, while logicans and model theorists do large parts do a deeper and thus less varied (relatively speaking) study of the long established strong first- or higher order logics. The answers in this logic SE questions are one among the most interesting on the platform. As is always the case with such broad questions on logic, one could now go down many rabbit holds. I might give a shoutout to Tarski's restricting theorem for strong logics. Decidability is also a question for type systems, if you just choose any.
- Along with the theme of restrictions, type checking of a term checks all it can, while with propositions, there's always many and different aspects of a structure you can validate. Again, here, if you make cuts and your type system admits subtyping and whatnot, I suppose you can take coarser views on terms here too.
- In the latter notion of "fit in", there's the concept of categoricity and one may try to reflect that in uniqueness types.
- If you have narrowed down a your logics of interest and decide you want to approach your question from a raw computation and "fit into" perspective, then the subject of abstract rewriting and rewriting systems, which may strike one as even more formal than subfields mathematical logic, may be down your alley.
Side note 1: The verification process in the latter case need not even be restricted to axioms but we can do that for any propositions.
Side note 2: I'm not a fan of your initial wording "checking whether a proof of a proposition is correct". I'd instead say "checking whether an expression is a proof of a proposition". I say that because if you use your language here, then we grant every term the status of being a "wrong proof" for almost all propositions. That's just a question of our language here, though.
edited Feb 9 at 6:21
user56834
3,29021253
answered Feb 3 at 11:03
Nikolaj-KNikolaj-K
5,96723069
edited Feb 9 at 6:21
user56834
3,29021253
edited Feb 9 at 6:21
user56834
3,29021253
edited Feb 9 at 6:21
user56834
3,29021253
3,29021253
answered Feb 3 at 11:03
Nikolaj-KNikolaj-K
5,96723069
answered Feb 3 at 11:03
Nikolaj-KNikolaj-K
5,96723069
answered Feb 3 at 11:03
Nikolaj-KNikolaj-K
5,96723069
5,96723069
1
$begingroup$
@user56834 That's a very dry and concise response for me giving you various pointers. Let me not take offense here and just reiterate that I think the two notions are captured by the task to evaluate a yes-or-no valued algorithm, and with type systems that algorithms comes with that system and with a general logic it might not exist at all. I'm not aware of work that explicitly tries to join those challanges.
$endgroup$
– Nikolaj-K
Feb 3 at 15:38
$begingroup$
I re-read it, and I admit I was being uncharitable. My apologies.
$endgroup$
– user56834
Feb 9 at 6:21
$begingroup$
What do you think of Alex Kruckman's answer?
$endgroup$
– user56834
Feb 9 at 6:22
add a comment |
1
$begingroup$
@user56834 That's a very dry and concise response for me giving you various pointers. Let me not take offense here and just reiterate that I think the two notions are captured by the task to evaluate a yes-or-no valued algorithm, and with type systems that algorithms comes with that system and with a general logic it might not exist at all. I'm not aware of work that explicitly tries to join those challanges.
$endgroup$
– Nikolaj-K
Feb 3 at 15:38
$begingroup$
I re-read it, and I admit I was being uncharitable. My apologies.
$endgroup$
– user56834
Feb 9 at 6:21
$begingroup$
What do you think of Alex Kruckman's answer?
$endgroup$
– user56834
Feb 9 at 6:22
1
1
$begingroup$
@user56834 That's a very dry and concise response for me giving you various pointers. Let me not take offense here and just reiterate that I think the two notions are captured by the task to evaluate a yes-or-no valued algorithm, and with type systems that algorithms comes with that system and with a general logic it might not exist at all. I'm not aware of work that explicitly tries to join those challanges.
$endgroup$
– Nikolaj-K
Feb 3 at 15:38
$begingroup$
@user56834 That's a very dry and concise response for me giving you various pointers. Let me not take offense here and just reiterate that I think the two notions are captured by the task to evaluate a yes-or-no valued algorithm, and with type systems that algorithms comes with that system and with a general logic it might not exist at all. I'm not aware of work that explicitly tries to join those challanges.
$endgroup$
– Nikolaj-K
Feb 3 at 15:38
$begingroup$
I re-read it, and I admit I was being uncharitable. My apologies.
$endgroup$
– user56834
Feb 9 at 6:21
$begingroup$
I re-read it, and I admit I was being uncharitable. My apologies.
$endgroup$
– user56834
Feb 9 at 6:21
$begingroup$
What do you think of Alex Kruckman's answer?
$endgroup$
– user56834
Feb 9 at 6:22
$begingroup$
What do you think of Alex Kruckman's answer?
$endgroup$
– user56834
Feb 9 at 6:22
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- 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.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3095310%2faxiom-checking-as-type-checking%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
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
$begingroup$
Related question: math.stackexchange.com/questions/1697288/…
$endgroup$
– user56834
Mar 25 at 12:23