What exactly is a first-order logic?Is First Order Logic (FOL) the only fundamental logic?Is First Order Logic (FOL) the only fundamental logic?What are the advantages to intentionally omit (small) parts from first order logic?Has anyone developed a “restricted English” notation for logic (first-order or otherwise)?How important are equality, functions and constants for first order logic?Is there any relation beetwen justification logic and type theory?Concerning the logical projection: How to express nullary and unary operations as binary operations?Calculus for Higher Order LogicWhat exactly are the identity rules in logic?Ontological status of variablesClassical logic, symbolic logic, higher-order logic, First-order logic? Learning from scratch
How well known and how commonly used was Huffman coding in 1979?
A player is constantly pestering me about rules, what do I do as a DM?
Do equal angles necessarily mean a polygon is regular?
Alphabet completion rate
How precise do models need to be for 3d printing?
Going to get married soon, should I do it on Dec 31 or Jan 1?
Smooth Julia set for quadratic polynomials
As a DM, how do you control a dysfunctional group wanting different things out of a game?
Is this one of the engines from the 9/11 aircraft?
How do I make a very short story impactful?
Importance of the principal bundle in Chern-Simons theory
What sort of mathematical problems are there in AI that people are working on?
What happens when I sacrifice a creature when my Teysa Karlov is on the battlefield?
Change the boot order with no option in UEFI settings
Can the negators "jamais, rien, personne, plus, ni, aucun" be used in a single sentence?
How risky is real estate?
Should I tell my insurance company I'm making payments on my new car?
Was there ever a name for the weapons of the Others?
Unusual mail headers, evidence of an attempted attack. Have I been pwned?
What are the benefits of using the X Card safety tool in comparison to plain communication?
Why is there no havdallah when going from Yom Tov into Shabbat?
Changing the opacity of lines on a plot based on their value
ては's role in this 「追いかけては来ないでしょう」
Should I include salary information on my CV?
What exactly is a first-order logic?
Is First Order Logic (FOL) the only fundamental logic?Is First Order Logic (FOL) the only fundamental logic?What are the advantages to intentionally omit (small) parts from first order logic?Has anyone developed a “restricted English” notation for logic (first-order or otherwise)?How important are equality, functions and constants for first order logic?Is there any relation beetwen justification logic and type theory?Concerning the logical projection: How to express nullary and unary operations as binary operations?Calculus for Higher Order LogicWhat exactly are the identity rules in logic?Ontological status of variablesClassical logic, symbolic logic, higher-order logic, First-order logic? Learning from scratch
.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty margin-bottom:0;
Can someone explain in simple terms what exactly is a first-order logic?
From my amateur standpoint, I think that first-order logic is a some kind of a system of symbols and general logical rules and operations defined on that set of symbols in such a way that a first-order logic has some expressional "power" (that is, some statements can be represented in first-order logic and some theorems about first-order logic can be deduced).
However, when it comes to theorems, that is where I am stuck, because, basically, I do not know what exactly can be proved in first-order logic, including theorems about statements in first-order logic and about compound statements, and also theorems about first-order logic itself.
So, can someone here give, in as simple as possible terms, an explanation and description of a first-order logic? Preferably, as short as possible one.
Also, is there only one first-order logic or there are many first-order logics, each differing from all the other in axioms that are used to build such a theory?
logic symbolic-logic philosophy-of-logic
New contributor
Grešnik is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
add a comment |
Can someone explain in simple terms what exactly is a first-order logic?
From my amateur standpoint, I think that first-order logic is a some kind of a system of symbols and general logical rules and operations defined on that set of symbols in such a way that a first-order logic has some expressional "power" (that is, some statements can be represented in first-order logic and some theorems about first-order logic can be deduced).
However, when it comes to theorems, that is where I am stuck, because, basically, I do not know what exactly can be proved in first-order logic, including theorems about statements in first-order logic and about compound statements, and also theorems about first-order logic itself.
So, can someone here give, in as simple as possible terms, an explanation and description of a first-order logic? Preferably, as short as possible one.
Also, is there only one first-order logic or there are many first-order logics, each differing from all the other in axioms that are used to build such a theory?
logic symbolic-logic philosophy-of-logic
New contributor
Grešnik is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
First order logic is a logic equivalent to a predicate calculus, a formal system with connectives and quantifiers, where one can only quantify over non-logical variables, but not over predicates. Some logical laws and rules of inference govern possible deductions. More broadly, systems built over it (by adding non-logical axioms) are called first order, e.g. Peano arithmetic and ZFC set theory.
– Conifold
Jun 15 at 6:38
See Is First Order Logic (FOL) the only fundamental logic ?
– Mauro ALLEGRANZA
Jun 15 at 7:55
add a comment |
Can someone explain in simple terms what exactly is a first-order logic?
From my amateur standpoint, I think that first-order logic is a some kind of a system of symbols and general logical rules and operations defined on that set of symbols in such a way that a first-order logic has some expressional "power" (that is, some statements can be represented in first-order logic and some theorems about first-order logic can be deduced).
However, when it comes to theorems, that is where I am stuck, because, basically, I do not know what exactly can be proved in first-order logic, including theorems about statements in first-order logic and about compound statements, and also theorems about first-order logic itself.
So, can someone here give, in as simple as possible terms, an explanation and description of a first-order logic? Preferably, as short as possible one.
Also, is there only one first-order logic or there are many first-order logics, each differing from all the other in axioms that are used to build such a theory?
logic symbolic-logic philosophy-of-logic
New contributor
Grešnik is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
Can someone explain in simple terms what exactly is a first-order logic?
From my amateur standpoint, I think that first-order logic is a some kind of a system of symbols and general logical rules and operations defined on that set of symbols in such a way that a first-order logic has some expressional "power" (that is, some statements can be represented in first-order logic and some theorems about first-order logic can be deduced).
However, when it comes to theorems, that is where I am stuck, because, basically, I do not know what exactly can be proved in first-order logic, including theorems about statements in first-order logic and about compound statements, and also theorems about first-order logic itself.
So, can someone here give, in as simple as possible terms, an explanation and description of a first-order logic? Preferably, as short as possible one.
Also, is there only one first-order logic or there are many first-order logics, each differing from all the other in axioms that are used to build such a theory?
logic symbolic-logic philosophy-of-logic
logic symbolic-logic philosophy-of-logic
New contributor
Grešnik is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
New contributor
Grešnik is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
edited Jun 15 at 8:20
Mauro ALLEGRANZA
28.4k2 gold badges20 silver badges68 bronze badges
28.4k2 gold badges20 silver badges68 bronze badges
New contributor
Grešnik is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked Jun 15 at 6:04
GrešnikGrešnik
1474 bronze badges
1474 bronze badges
New contributor
Grešnik is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
New contributor
Grešnik is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
First order logic is a logic equivalent to a predicate calculus, a formal system with connectives and quantifiers, where one can only quantify over non-logical variables, but not over predicates. Some logical laws and rules of inference govern possible deductions. More broadly, systems built over it (by adding non-logical axioms) are called first order, e.g. Peano arithmetic and ZFC set theory.
– Conifold
Jun 15 at 6:38
See Is First Order Logic (FOL) the only fundamental logic ?
– Mauro ALLEGRANZA
Jun 15 at 7:55
add a comment |
First order logic is a logic equivalent to a predicate calculus, a formal system with connectives and quantifiers, where one can only quantify over non-logical variables, but not over predicates. Some logical laws and rules of inference govern possible deductions. More broadly, systems built over it (by adding non-logical axioms) are called first order, e.g. Peano arithmetic and ZFC set theory.
– Conifold
Jun 15 at 6:38
See Is First Order Logic (FOL) the only fundamental logic ?
– Mauro ALLEGRANZA
Jun 15 at 7:55
First order logic is a logic equivalent to a predicate calculus, a formal system with connectives and quantifiers, where one can only quantify over non-logical variables, but not over predicates. Some logical laws and rules of inference govern possible deductions. More broadly, systems built over it (by adding non-logical axioms) are called first order, e.g. Peano arithmetic and ZFC set theory.
– Conifold
Jun 15 at 6:38
First order logic is a logic equivalent to a predicate calculus, a formal system with connectives and quantifiers, where one can only quantify over non-logical variables, but not over predicates. Some logical laws and rules of inference govern possible deductions. More broadly, systems built over it (by adding non-logical axioms) are called first order, e.g. Peano arithmetic and ZFC set theory.
– Conifold
Jun 15 at 6:38
See Is First Order Logic (FOL) the only fundamental logic ?
– Mauro ALLEGRANZA
Jun 15 at 7:55
See Is First Order Logic (FOL) the only fundamental logic ?
– Mauro ALLEGRANZA
Jun 15 at 7:55
add a comment |
1 Answer
1
active
oldest
votes
FOL is the natural logic environment to formalize mathematical theories.
The basic characteristic of predicate calculus is the use of quantifiers : first-order logic is predicate calculus where quantification is restricted to individual variables (variables ranging over "objects") and quantification over predicate variables (i.e. variables ranging over "properties") is not allowed.
Propositional calculus, instead, is only a "toy": it is based on a very simplified model of language that is not useful to develop interesting theories, but can be used efficiently to study the basic properties of a formal system : consistency, completeness, etc.
With FOL we have the "logical engine", i.e. the syntax of the language with axioms and rules, and we usually study it in a similar way to the study of propositional calculus, in order to understand the basic meta-logic properties.
When we study "pure" FOL, we define the derivability relation (⊢), where :
⊢ φ means : "formula φ is derivable in the calculus", and Γ ⊢ φ means : "formula φ is derivable in the calculus form the set Γ of assumptions".
With it we prove the fundamental Soundness and Completeness Theorem :
Γ ⊢ φ iff Γ ⊨ φ, where the symbol ⊨ means semantic consequence.
In addition to the study of "pure" predicate logic, we are interested to add to the "logical engine" suitable non-logical constants, like ∈ ("in"), the binary relation of set theory, or + and × ("plus" and "times"), the basic arithmetical operations, with suitable axioms that govern their behaviour.
Thus, according to the specific mathematical symbols and axioms introduced, we have different mathematical theories; when the collection of axioms is the first-order version of Peano's axioms, we have PA, i.e. first-order theory of arithmetic.
The same for ZF, i.e. Zermelo-Fraenkel Set Theory.
Unfortunately, not all interesting mathematical properties are expressible with FOL; see Second-order and Higher-order Logic.
You might want to define the ⊨ symbol before using it.
– Kevin
Jun 18 at 16:59
add a comment |
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/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
);
);
Grešnik is a new contributor. Be nice, and check out our Code of Conduct.
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%2f64018%2fwhat-exactly-is-a-first-order-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
FOL is the natural logic environment to formalize mathematical theories.
The basic characteristic of predicate calculus is the use of quantifiers : first-order logic is predicate calculus where quantification is restricted to individual variables (variables ranging over "objects") and quantification over predicate variables (i.e. variables ranging over "properties") is not allowed.
Propositional calculus, instead, is only a "toy": it is based on a very simplified model of language that is not useful to develop interesting theories, but can be used efficiently to study the basic properties of a formal system : consistency, completeness, etc.
With FOL we have the "logical engine", i.e. the syntax of the language with axioms and rules, and we usually study it in a similar way to the study of propositional calculus, in order to understand the basic meta-logic properties.
When we study "pure" FOL, we define the derivability relation (⊢), where :
⊢ φ means : "formula φ is derivable in the calculus", and Γ ⊢ φ means : "formula φ is derivable in the calculus form the set Γ of assumptions".
With it we prove the fundamental Soundness and Completeness Theorem :
Γ ⊢ φ iff Γ ⊨ φ, where the symbol ⊨ means semantic consequence.
In addition to the study of "pure" predicate logic, we are interested to add to the "logical engine" suitable non-logical constants, like ∈ ("in"), the binary relation of set theory, or + and × ("plus" and "times"), the basic arithmetical operations, with suitable axioms that govern their behaviour.
Thus, according to the specific mathematical symbols and axioms introduced, we have different mathematical theories; when the collection of axioms is the first-order version of Peano's axioms, we have PA, i.e. first-order theory of arithmetic.
The same for ZF, i.e. Zermelo-Fraenkel Set Theory.
Unfortunately, not all interesting mathematical properties are expressible with FOL; see Second-order and Higher-order Logic.
You might want to define the ⊨ symbol before using it.
– Kevin
Jun 18 at 16:59
add a comment |
FOL is the natural logic environment to formalize mathematical theories.
The basic characteristic of predicate calculus is the use of quantifiers : first-order logic is predicate calculus where quantification is restricted to individual variables (variables ranging over "objects") and quantification over predicate variables (i.e. variables ranging over "properties") is not allowed.
Propositional calculus, instead, is only a "toy": it is based on a very simplified model of language that is not useful to develop interesting theories, but can be used efficiently to study the basic properties of a formal system : consistency, completeness, etc.
With FOL we have the "logical engine", i.e. the syntax of the language with axioms and rules, and we usually study it in a similar way to the study of propositional calculus, in order to understand the basic meta-logic properties.
When we study "pure" FOL, we define the derivability relation (⊢), where :
⊢ φ means : "formula φ is derivable in the calculus", and Γ ⊢ φ means : "formula φ is derivable in the calculus form the set Γ of assumptions".
With it we prove the fundamental Soundness and Completeness Theorem :
Γ ⊢ φ iff Γ ⊨ φ, where the symbol ⊨ means semantic consequence.
In addition to the study of "pure" predicate logic, we are interested to add to the "logical engine" suitable non-logical constants, like ∈ ("in"), the binary relation of set theory, or + and × ("plus" and "times"), the basic arithmetical operations, with suitable axioms that govern their behaviour.
Thus, according to the specific mathematical symbols and axioms introduced, we have different mathematical theories; when the collection of axioms is the first-order version of Peano's axioms, we have PA, i.e. first-order theory of arithmetic.
The same for ZF, i.e. Zermelo-Fraenkel Set Theory.
Unfortunately, not all interesting mathematical properties are expressible with FOL; see Second-order and Higher-order Logic.
You might want to define the ⊨ symbol before using it.
– Kevin
Jun 18 at 16:59
add a comment |
FOL is the natural logic environment to formalize mathematical theories.
The basic characteristic of predicate calculus is the use of quantifiers : first-order logic is predicate calculus where quantification is restricted to individual variables (variables ranging over "objects") and quantification over predicate variables (i.e. variables ranging over "properties") is not allowed.
Propositional calculus, instead, is only a "toy": it is based on a very simplified model of language that is not useful to develop interesting theories, but can be used efficiently to study the basic properties of a formal system : consistency, completeness, etc.
With FOL we have the "logical engine", i.e. the syntax of the language with axioms and rules, and we usually study it in a similar way to the study of propositional calculus, in order to understand the basic meta-logic properties.
When we study "pure" FOL, we define the derivability relation (⊢), where :
⊢ φ means : "formula φ is derivable in the calculus", and Γ ⊢ φ means : "formula φ is derivable in the calculus form the set Γ of assumptions".
With it we prove the fundamental Soundness and Completeness Theorem :
Γ ⊢ φ iff Γ ⊨ φ, where the symbol ⊨ means semantic consequence.
In addition to the study of "pure" predicate logic, we are interested to add to the "logical engine" suitable non-logical constants, like ∈ ("in"), the binary relation of set theory, or + and × ("plus" and "times"), the basic arithmetical operations, with suitable axioms that govern their behaviour.
Thus, according to the specific mathematical symbols and axioms introduced, we have different mathematical theories; when the collection of axioms is the first-order version of Peano's axioms, we have PA, i.e. first-order theory of arithmetic.
The same for ZF, i.e. Zermelo-Fraenkel Set Theory.
Unfortunately, not all interesting mathematical properties are expressible with FOL; see Second-order and Higher-order Logic.
FOL is the natural logic environment to formalize mathematical theories.
The basic characteristic of predicate calculus is the use of quantifiers : first-order logic is predicate calculus where quantification is restricted to individual variables (variables ranging over "objects") and quantification over predicate variables (i.e. variables ranging over "properties") is not allowed.
Propositional calculus, instead, is only a "toy": it is based on a very simplified model of language that is not useful to develop interesting theories, but can be used efficiently to study the basic properties of a formal system : consistency, completeness, etc.
With FOL we have the "logical engine", i.e. the syntax of the language with axioms and rules, and we usually study it in a similar way to the study of propositional calculus, in order to understand the basic meta-logic properties.
When we study "pure" FOL, we define the derivability relation (⊢), where :
⊢ φ means : "formula φ is derivable in the calculus", and Γ ⊢ φ means : "formula φ is derivable in the calculus form the set Γ of assumptions".
With it we prove the fundamental Soundness and Completeness Theorem :
Γ ⊢ φ iff Γ ⊨ φ, where the symbol ⊨ means semantic consequence.
In addition to the study of "pure" predicate logic, we are interested to add to the "logical engine" suitable non-logical constants, like ∈ ("in"), the binary relation of set theory, or + and × ("plus" and "times"), the basic arithmetical operations, with suitable axioms that govern their behaviour.
Thus, according to the specific mathematical symbols and axioms introduced, we have different mathematical theories; when the collection of axioms is the first-order version of Peano's axioms, we have PA, i.e. first-order theory of arithmetic.
The same for ZF, i.e. Zermelo-Fraenkel Set Theory.
Unfortunately, not all interesting mathematical properties are expressible with FOL; see Second-order and Higher-order Logic.
edited 2 days ago
answered Jun 15 at 8:08
Mauro ALLEGRANZAMauro ALLEGRANZA
28.4k2 gold badges20 silver badges68 bronze badges
28.4k2 gold badges20 silver badges68 bronze badges
You might want to define the ⊨ symbol before using it.
– Kevin
Jun 18 at 16:59
add a comment |
You might want to define the ⊨ symbol before using it.
– Kevin
Jun 18 at 16:59
You might want to define the ⊨ symbol before using it.
– Kevin
Jun 18 at 16:59
You might want to define the ⊨ symbol before using it.
– Kevin
Jun 18 at 16:59
add a comment |
Grešnik is a new contributor. Be nice, and check out our Code of Conduct.
Grešnik is a new contributor. Be nice, and check out our Code of Conduct.
Grešnik is a new contributor. Be nice, and check out our Code of Conduct.
Grešnik is a new contributor. Be nice, and check out our Code of Conduct.
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%2f64018%2fwhat-exactly-is-a-first-order-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
First order logic is a logic equivalent to a predicate calculus, a formal system with connectives and quantifiers, where one can only quantify over non-logical variables, but not over predicates. Some logical laws and rules of inference govern possible deductions. More broadly, systems built over it (by adding non-logical axioms) are called first order, e.g. Peano arithmetic and ZFC set theory.
– Conifold
Jun 15 at 6:38
See Is First Order Logic (FOL) the only fundamental logic ?
– Mauro ALLEGRANZA
Jun 15 at 7:55