Proof Using Model UniverseHow to test a second order logic argument for validityHow does one contradiction in argument makes the argument valid?Transitive Incompleteness of Logical WFF's Due to Godel's Incompleteness TheoremCan Deduction for a Valid Argument produce the wrong conclusion?Without computers, how can you conjecture the (in)validity of a long convoluted argument in Predicate Logic?From given premises, how can you conjecture the conclusion before attempting any (dis)proof?Clear and canonical examples of analytical proofs in philosophyModal validity & vagueness
How did the Druids learn the Greek language by the time of Caesar's campaign in Gaul?
What's the difference between xxxx-client and xxxx-server packages?
Why isn't the WDC 65816 available in "externally" 16-bit versions?
Why didn't the 6502 have increase/decrease opcodes for A?
Sudden cheap travel?
How am I ever going to be able to "vet" 120,000+ lines of Composer PHP code not written by me?
Do any countries have a pensions system funded entirely by past contributions, rather than current taxes?
Which TOS episode is that gif of Spock turning around and raising eyebrow from?
How to change the font in LineLegend?
Why don't all States switch to all postal voting?
Why is JavaScript not compiled to bytecode before sending over the network?
Expectation of 500 coin flips after 500 realizations
Is there a higher incidence of electoral fraud in states that use all-mail voting?
Is rotating a pawn so that it faces a different direction and then moves in that direction technically permitted according to the 2018 FIDE Laws?
How to answer my 5 year old why I can tell her what she has to do and why she can't tell me
Party Time with Captain Pun
Is it okay to true (align) a wheel with a missing spoke?
Synergistic walls: How would they interact?
How to stretch this Venn diagram?
What's the meaning of "411 on the late-night drop box"?
Reimbursed more than my travel expenses for interview
Writing Vec compare in a more compact way
Exponent like 2^3 in SI
Smallest Fibonacci Multiples
Proof Using Model Universe
How to test a second order logic argument for validityHow does one contradiction in argument makes the argument valid?Transitive Incompleteness of Logical WFF's Due to Godel's Incompleteness TheoremCan Deduction for a Valid Argument produce the wrong conclusion?Without computers, how can you conjecture the (in)validity of a long convoluted argument in Predicate Logic?From given premises, how can you conjecture the conclusion before attempting any (dis)proof?Clear and canonical examples of analytical proofs in philosophyModal validity & vagueness
.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty
margin-bottom:0;
.everyonelovesstackoverflowposition:absolute;height:1px;width:1px;opacity:0;top:0;left:0;pointer-events:none;
Suppose I am trying to prove the following argument
(∀x)(Cx → Dx), (∀x)(Ex → ~Dx), /∴ (∀x)(Ex → ~Cx)
Now, let's also assume that I don't know if this argument is valid or not. Because of this, I try to check for invalidity using the model universe method (even though it would be easy enough to construct a direct proof).
I start by restricting the domain to D = a, and I check the following argument for a situation where I have true premises and a false conclusion.
Ca → Da, Ea → ~Da, /∴ Ea → ~Ca
Obviously, I can't find a counter-example, so I continue to expand the domain to D = a, b, D = a, b, c, etc.
Now, there is a theorem for the model universe method that states, "If n is the number of predicate variables in an argument, 2^n is the upper bound of elements you can test in a domain before you can determine that the argument is valid."
If I test the above argument using the model universe method to the point that my domain includes 8 (2^n) elements, have I just constructed a formal proof? Would I be able to use the model universe method as a means to formally prove an argument?
Thanks.
Edit:
This problem was not taken from a book, but we're going to define a formal proof as "a finite sequence of well-formed formulas, each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference." And yes, this is in the context of monadic predicate calculus.
logic proof predicate-logic
asked Sep 29 at 23:35
N. BarN. Bar
2276 bronze badges
add a comment
|
Suppose I am trying to prove the following argument
(∀x)(Cx → Dx), (∀x)(Ex → ~Dx), /∴ (∀x)(Ex → ~Cx)
Now, let's also assume that I don't know if this argument is valid or not. Because of this, I try to check for invalidity using the model universe method (even though it would be easy enough to construct a direct proof).
I start by restricting the domain to D = a, and I check the following argument for a situation where I have true premises and a false conclusion.
Ca → Da, Ea → ~Da, /∴ Ea → ~Ca
Obviously, I can't find a counter-example, so I continue to expand the domain to D = a, b, D = a, b, c, etc.
Now, there is a theorem for the model universe method that states, "If n is the number of predicate variables in an argument, 2^n is the upper bound of elements you can test in a domain before you can determine that the argument is valid."
If I test the above argument using the model universe method to the point that my domain includes 8 (2^n) elements, have I just constructed a formal proof? Would I be able to use the model universe method as a means to formally prove an argument?
Thanks.
Edit:
This problem was not taken from a book, but we're going to define a formal proof as "a finite sequence of well-formed formulas, each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference." And yes, this is in the context of monadic predicate calculus.
logic proof predicate-logic
asked Sep 29 at 23:35
N. BarN. Bar
2276 bronze badges
Are you following some text or other source? The answer may depend on what their definition of "formal proof" is.
– Conifold
Sep 29 at 23:58
@Conifold Thanks for your interest in the question. I just edited it for clarification.
– N. Bar
Sep 30 at 0:05
So are you only allowed to use axioms and rules of inference of monadic predicate calculus in a "formal proof"? Because setting up models and proving the completeness theorem you mentioned requires other means, such as set theory and maybe induction. Using them will not make a "formal proof in monadic predicate calculus".
– Conifold
Sep 30 at 0:10
add a comment
|
Suppose I am trying to prove the following argument
(∀x)(Cx → Dx), (∀x)(Ex → ~Dx), /∴ (∀x)(Ex → ~Cx)
Now, let's also assume that I don't know if this argument is valid or not. Because of this, I try to check for invalidity using the model universe method (even though it would be easy enough to construct a direct proof).
I start by restricting the domain to D = a, and I check the following argument for a situation where I have true premises and a false conclusion.
Ca → Da, Ea → ~Da, /∴ Ea → ~Ca
Obviously, I can't find a counter-example, so I continue to expand the domain to D = a, b, D = a, b, c, etc.
Now, there is a theorem for the model universe method that states, "If n is the number of predicate variables in an argument, 2^n is the upper bound of elements you can test in a domain before you can determine that the argument is valid."
If I test the above argument using the model universe method to the point that my domain includes 8 (2^n) elements, have I just constructed a formal proof? Would I be able to use the model universe method as a means to formally prove an argument?
Thanks.
Edit:
This problem was not taken from a book, but we're going to define a formal proof as "a finite sequence of well-formed formulas, each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference." And yes, this is in the context of monadic predicate calculus.
logic proof predicate-logic
asked Sep 29 at 23:35
N. BarN. Bar
2276 bronze badges
Suppose I am trying to prove the following argument
(∀x)(Cx → Dx), (∀x)(Ex → ~Dx), /∴ (∀x)(Ex → ~Cx)
Now, let's also assume that I don't know if this argument is valid or not. Because of this, I try to check for invalidity using the model universe method (even though it would be easy enough to construct a direct proof).
I start by restricting the domain to D = a, and I check the following argument for a situation where I have true premises and a false conclusion.
Ca → Da, Ea → ~Da, /∴ Ea → ~Ca
Obviously, I can't find a counter-example, so I continue to expand the domain to D = a, b, D = a, b, c, etc.
Now, there is a theorem for the model universe method that states, "If n is the number of predicate variables in an argument, 2^n is the upper bound of elements you can test in a domain before you can determine that the argument is valid."
If I test the above argument using the model universe method to the point that my domain includes 8 (2^n) elements, have I just constructed a formal proof? Would I be able to use the model universe method as a means to formally prove an argument?
Thanks.
Edit:
This problem was not taken from a book, but we're going to define a formal proof as "a finite sequence of well-formed formulas, each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference." And yes, this is in the context of monadic predicate calculus.
logic proof predicate-logic
logic proof predicate-logic
asked Sep 29 at 23:35
N. BarN. Bar
2276 bronze badges
asked Sep 29 at 23:35
N. BarN. Bar
2276 bronze badges
edited Sep 30 at 0:03
N. Bar
asked Sep 29 at 23:35
N. BarN. Bar
2276 bronze badges
asked Sep 29 at 23:35
N. BarN. Bar
2276 bronze badges
asked Sep 29 at 23:35
N. BarN. Bar
2276 bronze badges
2276 bronze badges
Are you following some text or other source? The answer may depend on what their definition of "formal proof" is.
– Conifold
Sep 29 at 23:58
@Conifold Thanks for your interest in the question. I just edited it for clarification.
– N. Bar
Sep 30 at 0:05
So are you only allowed to use axioms and rules of inference of monadic predicate calculus in a "formal proof"? Because setting up models and proving the completeness theorem you mentioned requires other means, such as set theory and maybe induction. Using them will not make a "formal proof in monadic predicate calculus".
– Conifold
Sep 30 at 0:10
add a comment
|
Are you following some text or other source? The answer may depend on what their definition of "formal proof" is.
– Conifold
Sep 29 at 23:58
@Conifold Thanks for your interest in the question. I just edited it for clarification.
– N. Bar
Sep 30 at 0:05
So are you only allowed to use axioms and rules of inference of monadic predicate calculus in a "formal proof"? Because setting up models and proving the completeness theorem you mentioned requires other means, such as set theory and maybe induction. Using them will not make a "formal proof in monadic predicate calculus".
– Conifold
Sep 30 at 0:10
Are you following some text or other source? The answer may depend on what their definition of "formal proof" is.
– Conifold
Sep 29 at 23:58
Are you following some text or other source? The answer may depend on what their definition of "formal proof" is.
– Conifold
Sep 29 at 23:58
@Conifold Thanks for your interest in the question. I just edited it for clarification.
– N. Bar
Sep 30 at 0:05
@Conifold Thanks for your interest in the question. I just edited it for clarification.
– N. Bar
Sep 30 at 0:05
So are you only allowed to use axioms and rules of inference of monadic predicate calculus in a "formal proof"? Because setting up models and proving the completeness theorem you mentioned requires other means, such as set theory and maybe induction. Using them will not make a "formal proof in monadic predicate calculus".
– Conifold
Sep 30 at 0:10
So are you only allowed to use axioms and rules of inference of monadic predicate calculus in a "formal proof"? Because setting up models and proving the completeness theorem you mentioned requires other means, such as set theory and maybe induction. Using them will not make a "formal proof in monadic predicate calculus".
– Conifold
Sep 30 at 0:10
add a comment
|
1 Answer
1
active
oldest
votes
Yes-ish: it takes some work to formalize it, but it can be done.
Specifically, the proof of the relevant model checking theorem gives a general method for proving, for an appropriate sentence p, a sentence of the form "If q_i implies p for each i < n, then p is true" where n is the appropriate bound and q_i: i < n are sentences characterizing each of the relevant finite isomorphism types. Each individual model check in turn is formalized as a proof of "q_i implies p." Putting this together gives a formal proof of p.
However, keep in mind that that theorem only holds when our language consists entirely of unary relation (or predicate, if you prefer) symbols. Since that's really a very rare situation, I'd say it's a good idea to avoid it when possible (especially in a case like this where it's much harder than the proof not using the theorem).
answered Sep 29 at 23:49
Noah SchweberNoah Schweber
7881 gold badge5 silver badges10 bronze badges
I am not sure what the intended meaning of a "formal proof" is in the OP. Using a model argument, even together with a proof of the completeness (meta)theorem, is not really a "formal proof" in the object theory (monadic predicate calculus, I presume).
– Conifold
Sep 29 at 23:57
@Conifold It is, though: for each of the finitely many isomorphism types we can find a sentence $psi$ characterizing it up to isomorphism (every finite structure in a finite language has such a sentence); the model checking then amounts to proving that each such $psi$ implies the theorem we want, together with the proof of the model checking theorem above. The casework is entirely formalizable inside the object theory.
– Noah Schweber
Sep 29 at 23:59
This uses metatheoretic means beyond the ones of the theory itself. I am just not sure what his textbook allows as "formal proofs". If it interprets "formal proof" as syntactic, semantic means are off-limits. But if it just means "rigorous" in some loose sense, they would be ok.
– Conifold
Sep 30 at 0:03
@Conifold See my edit.
– N. Bar
Sep 30 at 0:04
@Conifold No it doesn't: the formalized version of that instance of the model checking theorem does exactly this. It really is straightforwardly formalizable.
– Noah Schweber
Sep 30 at 0:04
|
show 6 more comments
Your Answer
StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "265"
;
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: false,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: null,
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/4.0/"u003ecc by-sa 4.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%2fphilosophy.stackexchange.com%2fquestions%2f67430%2fproof-using-model-universe%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
Yes-ish: it takes some work to formalize it, but it can be done.
Specifically, the proof of the relevant model checking theorem gives a general method for proving, for an appropriate sentence p, a sentence of the form "If q_i implies p for each i < n, then p is true" where n is the appropriate bound and q_i: i < n are sentences characterizing each of the relevant finite isomorphism types. Each individual model check in turn is formalized as a proof of "q_i implies p." Putting this together gives a formal proof of p.
However, keep in mind that that theorem only holds when our language consists entirely of unary relation (or predicate, if you prefer) symbols. Since that's really a very rare situation, I'd say it's a good idea to avoid it when possible (especially in a case like this where it's much harder than the proof not using the theorem).
answered Sep 29 at 23:49
Noah SchweberNoah Schweber
7881 gold badge5 silver badges10 bronze badges
I am not sure what the intended meaning of a "formal proof" is in the OP. Using a model argument, even together with a proof of the completeness (meta)theorem, is not really a "formal proof" in the object theory (monadic predicate calculus, I presume).
– Conifold
Sep 29 at 23:57
@Conifold It is, though: for each of the finitely many isomorphism types we can find a sentence $psi$ characterizing it up to isomorphism (every finite structure in a finite language has such a sentence); the model checking then amounts to proving that each such $psi$ implies the theorem we want, together with the proof of the model checking theorem above. The casework is entirely formalizable inside the object theory.
– Noah Schweber
Sep 29 at 23:59
This uses metatheoretic means beyond the ones of the theory itself. I am just not sure what his textbook allows as "formal proofs". If it interprets "formal proof" as syntactic, semantic means are off-limits. But if it just means "rigorous" in some loose sense, they would be ok.
– Conifold
Sep 30 at 0:03
@Conifold See my edit.
– N. Bar
Sep 30 at 0:04
@Conifold No it doesn't: the formalized version of that instance of the model checking theorem does exactly this. It really is straightforwardly formalizable.
– Noah Schweber
Sep 30 at 0:04
|
show 6 more comments
Yes-ish: it takes some work to formalize it, but it can be done.
Specifically, the proof of the relevant model checking theorem gives a general method for proving, for an appropriate sentence p, a sentence of the form "If q_i implies p for each i < n, then p is true" where n is the appropriate bound and q_i: i < n are sentences characterizing each of the relevant finite isomorphism types. Each individual model check in turn is formalized as a proof of "q_i implies p." Putting this together gives a formal proof of p.
However, keep in mind that that theorem only holds when our language consists entirely of unary relation (or predicate, if you prefer) symbols. Since that's really a very rare situation, I'd say it's a good idea to avoid it when possible (especially in a case like this where it's much harder than the proof not using the theorem).
answered Sep 29 at 23:49
Noah SchweberNoah Schweber
7881 gold badge5 silver badges10 bronze badges
I am not sure what the intended meaning of a "formal proof" is in the OP. Using a model argument, even together with a proof of the completeness (meta)theorem, is not really a "formal proof" in the object theory (monadic predicate calculus, I presume).
– Conifold
Sep 29 at 23:57
@Conifold It is, though: for each of the finitely many isomorphism types we can find a sentence $psi$ characterizing it up to isomorphism (every finite structure in a finite language has such a sentence); the model checking then amounts to proving that each such $psi$ implies the theorem we want, together with the proof of the model checking theorem above. The casework is entirely formalizable inside the object theory.
– Noah Schweber
Sep 29 at 23:59
This uses metatheoretic means beyond the ones of the theory itself. I am just not sure what his textbook allows as "formal proofs". If it interprets "formal proof" as syntactic, semantic means are off-limits. But if it just means "rigorous" in some loose sense, they would be ok.
– Conifold
Sep 30 at 0:03
@Conifold See my edit.
– N. Bar
Sep 30 at 0:04
@Conifold No it doesn't: the formalized version of that instance of the model checking theorem does exactly this. It really is straightforwardly formalizable.
– Noah Schweber
Sep 30 at 0:04
|
show 6 more comments
Yes-ish: it takes some work to formalize it, but it can be done.
Specifically, the proof of the relevant model checking theorem gives a general method for proving, for an appropriate sentence p, a sentence of the form "If q_i implies p for each i < n, then p is true" where n is the appropriate bound and q_i: i < n are sentences characterizing each of the relevant finite isomorphism types. Each individual model check in turn is formalized as a proof of "q_i implies p." Putting this together gives a formal proof of p.
However, keep in mind that that theorem only holds when our language consists entirely of unary relation (or predicate, if you prefer) symbols. Since that's really a very rare situation, I'd say it's a good idea to avoid it when possible (especially in a case like this where it's much harder than the proof not using the theorem).
answered Sep 29 at 23:49
Noah SchweberNoah Schweber
7881 gold badge5 silver badges10 bronze badges
Yes-ish: it takes some work to formalize it, but it can be done.
Specifically, the proof of the relevant model checking theorem gives a general method for proving, for an appropriate sentence p, a sentence of the form "If q_i implies p for each i < n, then p is true" where n is the appropriate bound and q_i: i < n are sentences characterizing each of the relevant finite isomorphism types. Each individual model check in turn is formalized as a proof of "q_i implies p." Putting this together gives a formal proof of p.
However, keep in mind that that theorem only holds when our language consists entirely of unary relation (or predicate, if you prefer) symbols. Since that's really a very rare situation, I'd say it's a good idea to avoid it when possible (especially in a case like this where it's much harder than the proof not using the theorem).
answered Sep 29 at 23:49
Noah SchweberNoah Schweber
7881 gold badge5 silver badges10 bronze badges
edited Sep 30 at 0:13
answered Sep 29 at 23:49
Noah SchweberNoah Schweber
7881 gold badge5 silver badges10 bronze badges
answered Sep 29 at 23:49
Noah SchweberNoah Schweber
7881 gold badge5 silver badges10 bronze badges
answered Sep 29 at 23:49
Noah SchweberNoah Schweber
7881 gold badge5 silver badges10 bronze badges
7881 gold badge5 silver badges10 bronze badges
I am not sure what the intended meaning of a "formal proof" is in the OP. Using a model argument, even together with a proof of the completeness (meta)theorem, is not really a "formal proof" in the object theory (monadic predicate calculus, I presume).
– Conifold
Sep 29 at 23:57
@Conifold It is, though: for each of the finitely many isomorphism types we can find a sentence $psi$ characterizing it up to isomorphism (every finite structure in a finite language has such a sentence); the model checking then amounts to proving that each such $psi$ implies the theorem we want, together with the proof of the model checking theorem above. The casework is entirely formalizable inside the object theory.
– Noah Schweber
Sep 29 at 23:59
This uses metatheoretic means beyond the ones of the theory itself. I am just not sure what his textbook allows as "formal proofs". If it interprets "formal proof" as syntactic, semantic means are off-limits. But if it just means "rigorous" in some loose sense, they would be ok.
– Conifold
Sep 30 at 0:03
@Conifold See my edit.
– N. Bar
Sep 30 at 0:04
@Conifold No it doesn't: the formalized version of that instance of the model checking theorem does exactly this. It really is straightforwardly formalizable.
– Noah Schweber
Sep 30 at 0:04
|
show 6 more comments
I am not sure what the intended meaning of a "formal proof" is in the OP. Using a model argument, even together with a proof of the completeness (meta)theorem, is not really a "formal proof" in the object theory (monadic predicate calculus, I presume).
– Conifold
Sep 29 at 23:57
@Conifold It is, though: for each of the finitely many isomorphism types we can find a sentence $psi$ characterizing it up to isomorphism (every finite structure in a finite language has such a sentence); the model checking then amounts to proving that each such $psi$ implies the theorem we want, together with the proof of the model checking theorem above. The casework is entirely formalizable inside the object theory.
– Noah Schweber
Sep 29 at 23:59
This uses metatheoretic means beyond the ones of the theory itself. I am just not sure what his textbook allows as "formal proofs". If it interprets "formal proof" as syntactic, semantic means are off-limits. But if it just means "rigorous" in some loose sense, they would be ok.
– Conifold
Sep 30 at 0:03
@Conifold See my edit.
– N. Bar
Sep 30 at 0:04
@Conifold No it doesn't: the formalized version of that instance of the model checking theorem does exactly this. It really is straightforwardly formalizable.
– Noah Schweber
Sep 30 at 0:04
I am not sure what the intended meaning of a "formal proof" is in the OP. Using a model argument, even together with a proof of the completeness (meta)theorem, is not really a "formal proof" in the object theory (monadic predicate calculus, I presume).
– Conifold
Sep 29 at 23:57
I am not sure what the intended meaning of a "formal proof" is in the OP. Using a model argument, even together with a proof of the completeness (meta)theorem, is not really a "formal proof" in the object theory (monadic predicate calculus, I presume).
– Conifold
Sep 29 at 23:57
@Conifold It is, though: for each of the finitely many isomorphism types we can find a sentence $psi$ characterizing it up to isomorphism (every finite structure in a finite language has such a sentence); the model checking then amounts to proving that each such $psi$ implies the theorem we want, together with the proof of the model checking theorem above. The casework is entirely formalizable inside the object theory.
– Noah Schweber
Sep 29 at 23:59
@Conifold It is, though: for each of the finitely many isomorphism types we can find a sentence $psi$ characterizing it up to isomorphism (every finite structure in a finite language has such a sentence); the model checking then amounts to proving that each such $psi$ implies the theorem we want, together with the proof of the model checking theorem above. The casework is entirely formalizable inside the object theory.
– Noah Schweber
Sep 29 at 23:59
This uses metatheoretic means beyond the ones of the theory itself. I am just not sure what his textbook allows as "formal proofs". If it interprets "formal proof" as syntactic, semantic means are off-limits. But if it just means "rigorous" in some loose sense, they would be ok.
– Conifold
Sep 30 at 0:03
This uses metatheoretic means beyond the ones of the theory itself. I am just not sure what his textbook allows as "formal proofs". If it interprets "formal proof" as syntactic, semantic means are off-limits. But if it just means "rigorous" in some loose sense, they would be ok.
– Conifold
Sep 30 at 0:03
@Conifold See my edit.
– N. Bar
Sep 30 at 0:04
@Conifold See my edit.
– N. Bar
Sep 30 at 0:04
@Conifold No it doesn't: the formalized version of that instance of the model checking theorem does exactly this. It really is straightforwardly formalizable.
– Noah Schweber
Sep 30 at 0:04
@Conifold No it doesn't: the formalized version of that instance of the model checking theorem does exactly this. It really is straightforwardly formalizable.
– Noah Schweber
Sep 30 at 0:04
|
show 6 more comments
Thanks for contributing an answer to Philosophy 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.
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%2fphilosophy.stackexchange.com%2fquestions%2f67430%2fproof-using-model-universe%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
Are you following some text or other source? The answer may depend on what their definition of "formal proof" is.
– Conifold
Sep 29 at 23:58
@Conifold Thanks for your interest in the question. I just edited it for clarification.
– N. Bar
Sep 30 at 0:05
So are you only allowed to use axioms and rules of inference of monadic predicate calculus in a "formal proof"? Because setting up models and proving the completeness theorem you mentioned requires other means, such as set theory and maybe induction. Using them will not make a "formal proof in monadic predicate calculus".
– Conifold
Sep 30 at 0:10