First order theory for a given sentential logic
$begingroup$
Is it possible to extract the axioms and inference rules of a sentential/zeroth-order logic into a first order theory? Does this kind of "hoisting" have a name?
I'm trying to figure out how to check whether a finitely-valued sentential logic is consistent with an arbitrary collection of axioms and inference rules. I'd like to, if possible, use the same machinery for checking both the axioms and the inference rules.
I think that's equivalent to asking if the finitely-valued semantics is complete. I'm not trying to tackle soundness with this construction.
Let bold ($mathbf{I}$) Łukasiewicz-style operators represent logical connectives in the finitely-valued sentential logic under examination and $land, lor, to$ represent connectives in classical logic. $mathbf{I}$ is a logical symbol in the logic under examination, but a function symbol in the first-order theory.
Modus ponens in logic under examination:
$$ frac{a ;;text{and};; mathbf{I} a b}{b} $$
Weakining (as a tautology)
$$ frac{cdot}{mathbf{I}amathbf{I}ba} $$
Written as laws in a first order theory with $D$ being the domain of truth values in the logic under examination and $T$ being a predicate that identifies designated truth values in $D$ .
"Hoisting" of modus ponens. Because it's an inference rule, we consider the truth-ness of the premises and the conclusion independently.
$$ forall ab mathop{:} D mathop{.} ; T(a) land T(mathbf{I}ab) to T(b) $$
"Hoisting" of weakening. Because it's only intended to be a tautology, we check the truth-ness of the expression at the very end.
$$ forall a b mathop{:} D mathop{.} ; T[mathbf{I}amathbf{I}ba] $$
logic
asked Dec 9 '18 at 19:31
Gregory NisbetGregory Nisbet
756612
$endgroup$
add a comment |
$begingroup$
Is it possible to extract the axioms and inference rules of a sentential/zeroth-order logic into a first order theory? Does this kind of "hoisting" have a name?
I'm trying to figure out how to check whether a finitely-valued sentential logic is consistent with an arbitrary collection of axioms and inference rules. I'd like to, if possible, use the same machinery for checking both the axioms and the inference rules.
I think that's equivalent to asking if the finitely-valued semantics is complete. I'm not trying to tackle soundness with this construction.
Let bold ($mathbf{I}$) Łukasiewicz-style operators represent logical connectives in the finitely-valued sentential logic under examination and $land, lor, to$ represent connectives in classical logic. $mathbf{I}$ is a logical symbol in the logic under examination, but a function symbol in the first-order theory.
Modus ponens in logic under examination:
$$ frac{a ;;text{and};; mathbf{I} a b}{b} $$
Weakining (as a tautology)
$$ frac{cdot}{mathbf{I}amathbf{I}ba} $$
Written as laws in a first order theory with $D$ being the domain of truth values in the logic under examination and $T$ being a predicate that identifies designated truth values in $D$ .
"Hoisting" of modus ponens. Because it's an inference rule, we consider the truth-ness of the premises and the conclusion independently.
$$ forall ab mathop{:} D mathop{.} ; T(a) land T(mathbf{I}ab) to T(b) $$
"Hoisting" of weakening. Because it's only intended to be a tautology, we check the truth-ness of the expression at the very end.
$$ forall a b mathop{:} D mathop{.} ; T[mathbf{I}amathbf{I}ba] $$
logic
asked Dec 9 '18 at 19:31
Gregory NisbetGregory Nisbet
756612
$endgroup$
1
$begingroup$
As an aside to my answer below: what you call "implication introduction" is usually known as "weakening". "Implication introduction" is usually used as the name of an inference rule in natural deduction.
$endgroup$
– Rob Arthan
Dec 9 '18 at 22:25
add a comment |
$begingroup$
Is it possible to extract the axioms and inference rules of a sentential/zeroth-order logic into a first order theory? Does this kind of "hoisting" have a name?
I'm trying to figure out how to check whether a finitely-valued sentential logic is consistent with an arbitrary collection of axioms and inference rules. I'd like to, if possible, use the same machinery for checking both the axioms and the inference rules.
I think that's equivalent to asking if the finitely-valued semantics is complete. I'm not trying to tackle soundness with this construction.
Let bold ($mathbf{I}$) Łukasiewicz-style operators represent logical connectives in the finitely-valued sentential logic under examination and $land, lor, to$ represent connectives in classical logic. $mathbf{I}$ is a logical symbol in the logic under examination, but a function symbol in the first-order theory.
Modus ponens in logic under examination:
$$ frac{a ;;text{and};; mathbf{I} a b}{b} $$
Weakining (as a tautology)
$$ frac{cdot}{mathbf{I}amathbf{I}ba} $$
Written as laws in a first order theory with $D$ being the domain of truth values in the logic under examination and $T$ being a predicate that identifies designated truth values in $D$ .
"Hoisting" of modus ponens. Because it's an inference rule, we consider the truth-ness of the premises and the conclusion independently.
$$ forall ab mathop{:} D mathop{.} ; T(a) land T(mathbf{I}ab) to T(b) $$
"Hoisting" of weakening. Because it's only intended to be a tautology, we check the truth-ness of the expression at the very end.
$$ forall a b mathop{:} D mathop{.} ; T[mathbf{I}amathbf{I}ba] $$
logic
asked Dec 9 '18 at 19:31
Gregory NisbetGregory Nisbet
756612
$endgroup$
Is it possible to extract the axioms and inference rules of a sentential/zeroth-order logic into a first order theory? Does this kind of "hoisting" have a name?
I'm trying to figure out how to check whether a finitely-valued sentential logic is consistent with an arbitrary collection of axioms and inference rules. I'd like to, if possible, use the same machinery for checking both the axioms and the inference rules.
I think that's equivalent to asking if the finitely-valued semantics is complete. I'm not trying to tackle soundness with this construction.
Let bold ($mathbf{I}$) Łukasiewicz-style operators represent logical connectives in the finitely-valued sentential logic under examination and $land, lor, to$ represent connectives in classical logic. $mathbf{I}$ is a logical symbol in the logic under examination, but a function symbol in the first-order theory.
Modus ponens in logic under examination:
$$ frac{a ;;text{and};; mathbf{I} a b}{b} $$
Weakining (as a tautology)
$$ frac{cdot}{mathbf{I}amathbf{I}ba} $$
Written as laws in a first order theory with $D$ being the domain of truth values in the logic under examination and $T$ being a predicate that identifies designated truth values in $D$ .
"Hoisting" of modus ponens. Because it's an inference rule, we consider the truth-ness of the premises and the conclusion independently.
$$ forall ab mathop{:} D mathop{.} ; T(a) land T(mathbf{I}ab) to T(b) $$
"Hoisting" of weakening. Because it's only intended to be a tautology, we check the truth-ness of the expression at the very end.
$$ forall a b mathop{:} D mathop{.} ; T[mathbf{I}amathbf{I}ba] $$
logic
logic
asked Dec 9 '18 at 19:31
Gregory NisbetGregory Nisbet
756612
asked Dec 9 '18 at 19:31
Gregory NisbetGregory Nisbet
756612
edited Dec 9 '18 at 22:26
Gregory Nisbet
asked Dec 9 '18 at 19:31
Gregory NisbetGregory Nisbet
756612
asked Dec 9 '18 at 19:31
Gregory NisbetGregory Nisbet
756612
asked Dec 9 '18 at 19:31
Gregory NisbetGregory Nisbet
756612
756612
1
$begingroup$
As an aside to my answer below: what you call "implication introduction" is usually known as "weakening". "Implication introduction" is usually used as the name of an inference rule in natural deduction.
$endgroup$
– Rob Arthan
Dec 9 '18 at 22:25
add a comment |
1
$begingroup$
As an aside to my answer below: what you call "implication introduction" is usually known as "weakening". "Implication introduction" is usually used as the name of an inference rule in natural deduction.
$endgroup$
– Rob Arthan
Dec 9 '18 at 22:25
1
1
$begingroup$
As an aside to my answer below: what you call "implication introduction" is usually known as "weakening". "Implication introduction" is usually used as the name of an inference rule in natural deduction.
$endgroup$
– Rob Arthan
Dec 9 '18 at 22:25
$begingroup$
As an aside to my answer below: what you call "implication introduction" is usually known as "weakening". "Implication introduction" is usually used as the name of an inference rule in natural deduction.
$endgroup$
– Rob Arthan
Dec 9 '18 at 22:25
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
Yes, it is usually possible to model a propositional logic as a first-order theory whose domain of discourse represents the set of truth-values in the propositional logic and whose axioms represent the propositional axioms and inference rules. (I say "usually" because you could devise a bizarre propositional logic with side-conditions on the inference rules that would make them hard to model.)
I don't know of a name for this process in general, but for a large class of propositional logics, the first-order theory will be an equational theory of the sort studied in universal algebra, and the process amounts to giving an algebraic semantics for the logic. E.g., classical propositional logic corresponds to the theory of Boolean algebras and intuitionistic propositional logic corresponds to the theory of Heyting algebras.
answered Dec 9 '18 at 22:23
Rob ArthanRob Arthan
29.5k42967
$endgroup$
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%2f3032848%2ffirst-order-theory-for-a-given-sentential-logic%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
Yes, it is usually possible to model a propositional logic as a first-order theory whose domain of discourse represents the set of truth-values in the propositional logic and whose axioms represent the propositional axioms and inference rules. (I say "usually" because you could devise a bizarre propositional logic with side-conditions on the inference rules that would make them hard to model.)
I don't know of a name for this process in general, but for a large class of propositional logics, the first-order theory will be an equational theory of the sort studied in universal algebra, and the process amounts to giving an algebraic semantics for the logic. E.g., classical propositional logic corresponds to the theory of Boolean algebras and intuitionistic propositional logic corresponds to the theory of Heyting algebras.
answered Dec 9 '18 at 22:23
Rob ArthanRob Arthan
29.5k42967
$endgroup$
add a comment |
$begingroup$
Yes, it is usually possible to model a propositional logic as a first-order theory whose domain of discourse represents the set of truth-values in the propositional logic and whose axioms represent the propositional axioms and inference rules. (I say "usually" because you could devise a bizarre propositional logic with side-conditions on the inference rules that would make them hard to model.)
I don't know of a name for this process in general, but for a large class of propositional logics, the first-order theory will be an equational theory of the sort studied in universal algebra, and the process amounts to giving an algebraic semantics for the logic. E.g., classical propositional logic corresponds to the theory of Boolean algebras and intuitionistic propositional logic corresponds to the theory of Heyting algebras.
answered Dec 9 '18 at 22:23
Rob ArthanRob Arthan
29.5k42967
$endgroup$
add a comment |
$begingroup$
Yes, it is usually possible to model a propositional logic as a first-order theory whose domain of discourse represents the set of truth-values in the propositional logic and whose axioms represent the propositional axioms and inference rules. (I say "usually" because you could devise a bizarre propositional logic with side-conditions on the inference rules that would make them hard to model.)
I don't know of a name for this process in general, but for a large class of propositional logics, the first-order theory will be an equational theory of the sort studied in universal algebra, and the process amounts to giving an algebraic semantics for the logic. E.g., classical propositional logic corresponds to the theory of Boolean algebras and intuitionistic propositional logic corresponds to the theory of Heyting algebras.
answered Dec 9 '18 at 22:23
Rob ArthanRob Arthan
29.5k42967
$endgroup$
Yes, it is usually possible to model a propositional logic as a first-order theory whose domain of discourse represents the set of truth-values in the propositional logic and whose axioms represent the propositional axioms and inference rules. (I say "usually" because you could devise a bizarre propositional logic with side-conditions on the inference rules that would make them hard to model.)
I don't know of a name for this process in general, but for a large class of propositional logics, the first-order theory will be an equational theory of the sort studied in universal algebra, and the process amounts to giving an algebraic semantics for the logic. E.g., classical propositional logic corresponds to the theory of Boolean algebras and intuitionistic propositional logic corresponds to the theory of Heyting algebras.
answered Dec 9 '18 at 22:23
Rob ArthanRob Arthan
29.5k42967
answered Dec 9 '18 at 22:23
Rob ArthanRob Arthan
29.5k42967
answered Dec 9 '18 at 22:23
Rob ArthanRob Arthan
29.5k42967
answered Dec 9 '18 at 22:23
Rob ArthanRob Arthan
29.5k42967
29.5k42967
add a comment |
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%2f3032848%2ffirst-order-theory-for-a-given-sentential-logic%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
1
$begingroup$
As an aside to my answer below: what you call "implication introduction" is usually known as "weakening". "Implication introduction" is usually used as the name of an inference rule in natural deduction.
$endgroup$
– Rob Arthan
Dec 9 '18 at 22:25