Difference between revisions of "Notes:First order language"

From Maths
Jump to: navigation, search
(Saving work)
 
m (Alec moved page Notes:First order langauge to Notes:First order language without leaving a redirect: Typo in name, 33 views)
 
(One intermediate revision by the same user not shown)
Line 1: Line 1:
−
: '''Source: ''' [[Books:A Course on Mathematical Logic - Shashi Mohan Srivastava]]
+
: '''Sources: '''
 +
:# [[Books:A Course on Mathematical Logic - Shashi Mohan Srivastava]](ref<ref name="SMS">[[Books:A Course on Mathematical Logic - Shashi Mohan Srivastava]]</ref>)
 +
:# [[Books:Mathematical Logic - Foundations for Information Science - Wei Li]](ref<ref name="WL">[[Books:Mathematical Logic - Foundations for Information Science - Wei Li]]</ref>)
 +
The reference<ref name="Both">[[Books:A Course on Mathematical Logic - Shashi Mohan Srivastava]] and [[Books:Mathematical Logic - Foundations for Information Science - Wei Li]]</ref> will be used when the books agree.
 +
<!--
 +
NOTE TO EDITORS:
 +
The reference names used on this page are not the usual ones, as this is just a notes page
 +
-->
 +
==Summary==
 +
From my reading I can basically conclude:
 +
* We define first order languages according to a grammar, anything that results from this is a thing in the language, regardless of whether or not it is "utter crap" and the problem of saying whether something is true or false isn't easy, perhaps even possible, but we can say "given this (these) thing(s) then this other thing follows"
 +
==Definitions==
 +
===First Order Language===
 +
The references have not been closely compared and were studied separately (months apart)
 +
A ''first order language'' consists of two types of symbol<ref name="Both"/>:
 +
# Logical symbols<ref name="Both"/> (which are the same for all FOLs<ref name="Both"/>)
 +
## Variable symbols<ref name="Both"/> - at most countably many and may be empty<ref name="WL"/>, {{M|x_1,x_2,\ldots}} used for both. The {{M|x_1,x_2,\ldots}} order is called the alphabetical order<ref name="SMS"/>
 +
## Logical connective symbols - Which are: {{M|1=\neg,\ \wedge,\ \vee,\ \rightarrow}} and {{M|\leftrightarrow}}
 +
##* Disputed, <ref name="SMS"/> uses few (2) connectives and shows the rest can be constructed from these. It should be easy to "unify them"
 +
## Quantifier symbols - {{M|\forall}} and {{M|\exists}}
 +
## Equality symbol - the set containing {{M|\doteq}}<ref name="WL"/><ref group="Note">This is done so the author can unambiguously use {{M|1==}} in the "symbols" sense (these are the same) and {{M|1==}} in the sense of "in the FOL we can show these are equal".</ref>
 +
## Parenthesis symbols - {{M|(}} and {{M|)}}<ref name="WL"/>
 +
# Non-logical symbols<ref name="Both"/> (which vary from theory to theory<ref name="Both"/>), there are 3 kinds<ref name="WL"/>
 +
## {{M|\mathscr{L}_c}} - the set of constant symbols, at most countably many of them, {{M|c_1,c_2,\ldots}}<ref name="WL"/>
 +
## {{M|\mathscr{L}_f}} - the set of function symbols, at most countably many of them, {{M|f_1,f_2,\ldots}}, {{M|fx_1\ldots x_m}} denotes an {{M|m}}-ary function symbol, for {{M|m\ge 1}} being the number of variable symbols as well as the number of arguments to the function<ref name="WL"/>
 +
## {{M|\mathscr{L}_p}} - the set of predicate symbols, at most countably many of them, {{M|P_1,P_2,\ldots}}, {{M|Px_1,\ldots x_m}} denotes an {{M|m}}-ary predicate symbol for {{M|m\ge 1}} being the number of variable symbols as well as the number of arguments to the predicate<ref name="WL"/>
 +
We shall use {{M|\mathscr{L} }} to represent a FOL<ref name="WL"/>
 +
===Terms===
 +
The terms of a FOL, {{M|\mathscr{L} }} are defined inductively as follows<ref name="WL"/>:
 +
# {{M|\mathrm{T}_1}} - Each constant symbol is a term
 +
# {{M|\mathrm{T}_2}} - Each variable symbol is a term
 +
# {{M|\mathrm{T}_3}} - If {{M|t_1,\ldots,t_n}} are terms and {{M|f}} is an {{M|n}}-ary function symbol, then {{M|ft_1,\ldots t_n}} is a term.
 +
{{M|\mathscr{L}_\mathrm{T} }} denotes the set of all terms of a FOL {{M|\mathscr{L} }}<ref name="WL"/>. There is a BNF form of these, but it is trivial to show from the above so I wont rewrite it.
 +
: {{Note|It seems that it is impossible to write crap at this point as a term is just a variable, or a constant, of a function of some (functions of) variables and constants.}}
 +
===Logical formulas===
 +
The ''logical formulas'' of a FOL {{M|\mathscr{L} }} (or just "formulas" for short) will be represented by uppercase symbols, {{M|A,\ B,\ldots}}, They are defined inductively as follows<ref name="WL"/>:
 +
# {{M|\mathrm{F}_1}} - For {{M|t_1,t_2\in\mathscr{L}_\mathrm{T} }} then {{M|t_1\doteq t_2}} is a formula.
 +
# {{M|\mathrm{F}_2}} - For {{M|t_1,\ldots,t_n\in\mathscr{L}_\mathrm{T} }} and {{M|P}} is an {{M|n}}-ary predicate, {{M|Pt_1\ldots t_n}} is a formula.
 +
# {{M|\mathrm{F}_3}} - If {{M|A}} is a formula, then so is {{M|(\neg A)}}
 +
# {{M|\mathrm{F}_4}} - If {{M|A}} and {{M|B}} are formulas, then so are {{M|(A\wedge B)}}, {{M|(A\vee B)}}, {{M|(A\rightarrow B)}} and {{M|(A\leftrightarrow B)}}
 +
# {{M|\mathrm{F}_5}} - If {{M|A}} is a formula and {{M|x}} a variable, then both {{M|\forall xA}} and {{M|\exists xA}} are formulas. We call {{M|x}} a ''bound variable''
 +
Additionally:
 +
* Formulas defined by just {{M|\mathrm{F}_1}} and {{M|\mathrm{F}_2}} are called ''atomic formulas''; the rest are ''composite formulas''<ref name="WL"/>.
 +
{{M|\mathscr{L}_\mathrm{F} }} denotes the set of formulas of a FOL {{M|\mathscr{L} }}.
 +
: {{Note|Crap is now possible; like {{M|(x\doteq y)\wedge(x\not\doteq y)}}, however there are 2 kinds of crap, the first is that which is ''always'' crap, like the example I just gave, and some things which are crap given a certain set of assumptions}}
 +
==Notes==
 +
<references group="Note"/>
 +
==References==
 +
<references/>
 +
<hr/>
 +
=OLD PAGE=
 +
All from [[Books:A Course on Mathematical Logic - Shashi Mohan Srivastava]]
 
==Definition==
 
==Definition==
 
A [[first order language]], {{M|L}}, consists of two types of symbols:
 
A [[first order language]], {{M|L}}, consists of two types of symbols:

Latest revision as of 09:22, 28 August 2016

Sources:
  1. Books:A Course on Mathematical Logic - Shashi Mohan Srivastava(ref[1])
  2. Books:Mathematical Logic - Foundations for Information Science - Wei Li(ref[2])

The reference[3] will be used when the books agree.

Summary

From my reading I can basically conclude:

  • We define first order languages according to a grammar, anything that results from this is a thing in the language, regardless of whether or not it is "utter crap" and the problem of saying whether something is true or false isn't easy, perhaps even possible, but we can say "given this (these) thing(s) then this other thing follows"

Definitions

First Order Language

The references have not been closely compared and were studied separately (months apart) A first order language consists of two types of symbol[3]:

  1. Logical symbols[3] (which are the same for all FOLs[3])
    1. Variable symbols[3] - at most countably many and may be empty[2], [ilmath]x_1,x_2,\ldots[/ilmath] used for both. The [ilmath]x_1,x_2,\ldots[/ilmath] order is called the alphabetical order[1]
    2. Logical connective symbols - Which are: [ilmath]\neg,\ \wedge,\ \vee,\ \rightarrow[/ilmath] and [ilmath]\leftrightarrow[/ilmath]
      • Disputed, [1] uses few (2) connectives and shows the rest can be constructed from these. It should be easy to "unify them"
    3. Quantifier symbols - [ilmath]\forall[/ilmath] and [ilmath]\exists[/ilmath]
    4. Equality symbol - the set containing [ilmath]\doteq[/ilmath][2][Note 1]
    5. Parenthesis symbols - [ilmath]([/ilmath] and [ilmath])[/ilmath][2]
  2. Non-logical symbols[3] (which vary from theory to theory[3]), there are 3 kinds[2]
    1. [ilmath]\mathscr{L}_c[/ilmath] - the set of constant symbols, at most countably many of them, [ilmath]c_1,c_2,\ldots[/ilmath][2]
    2. [ilmath]\mathscr{L}_f[/ilmath] - the set of function symbols, at most countably many of them, [ilmath]f_1,f_2,\ldots[/ilmath], [ilmath]fx_1\ldots x_m[/ilmath] denotes an [ilmath]m[/ilmath]-ary function symbol, for [ilmath]m\ge 1[/ilmath] being the number of variable symbols as well as the number of arguments to the function[2]
    3. [ilmath]\mathscr{L}_p[/ilmath] - the set of predicate symbols, at most countably many of them, [ilmath]P_1,P_2,\ldots[/ilmath], [ilmath]Px_1,\ldots x_m[/ilmath] denotes an [ilmath]m[/ilmath]-ary predicate symbol for [ilmath]m\ge 1[/ilmath] being the number of variable symbols as well as the number of arguments to the predicate[2]

We shall use [ilmath]\mathscr{L} [/ilmath] to represent a FOL[2]

Terms

The terms of a FOL, [ilmath]\mathscr{L} [/ilmath] are defined inductively as follows[2]:

  1. [ilmath]\mathrm{T}_1[/ilmath] - Each constant symbol is a term
  2. [ilmath]\mathrm{T}_2[/ilmath] - Each variable symbol is a term
  3. [ilmath]\mathrm{T}_3[/ilmath] - If [ilmath]t_1,\ldots,t_n[/ilmath] are terms and [ilmath]f[/ilmath] is an [ilmath]n[/ilmath]-ary function symbol, then [ilmath]ft_1,\ldots t_n[/ilmath] is a term.

[ilmath]\mathscr{L}_\mathrm{T} [/ilmath] denotes the set of all terms of a FOL [ilmath]\mathscr{L} [/ilmath][2]. There is a BNF form of these, but it is trivial to show from the above so I wont rewrite it.

It seems that it is impossible to write crap at this point as a term is just a variable, or a constant, of a function of some (functions of) variables and constants.

Logical formulas

The logical formulas of a FOL [ilmath]\mathscr{L} [/ilmath] (or just "formulas" for short) will be represented by uppercase symbols, [ilmath]A,\ B,\ldots[/ilmath], They are defined inductively as follows[2]:

  1. [ilmath]\mathrm{F}_1[/ilmath] - For [ilmath]t_1,t_2\in\mathscr{L}_\mathrm{T} [/ilmath] then [ilmath]t_1\doteq t_2[/ilmath] is a formula.
  2. [ilmath]\mathrm{F}_2[/ilmath] - For [ilmath]t_1,\ldots,t_n\in\mathscr{L}_\mathrm{T} [/ilmath] and [ilmath]P[/ilmath] is an [ilmath]n[/ilmath]-ary predicate, [ilmath]Pt_1\ldots t_n[/ilmath] is a formula.
  3. [ilmath]\mathrm{F}_3[/ilmath] - If [ilmath]A[/ilmath] is a formula, then so is [ilmath](\neg A)[/ilmath]
  4. [ilmath]\mathrm{F}_4[/ilmath] - If [ilmath]A[/ilmath] and [ilmath]B[/ilmath] are formulas, then so are [ilmath](A\wedge B)[/ilmath], [ilmath](A\vee B)[/ilmath], [ilmath](A\rightarrow B)[/ilmath] and [ilmath](A\leftrightarrow B)[/ilmath]
  5. [ilmath]\mathrm{F}_5[/ilmath] - If [ilmath]A[/ilmath] is a formula and [ilmath]x[/ilmath] a variable, then both [ilmath]\forall xA[/ilmath] and [ilmath]\exists xA[/ilmath] are formulas. We call [ilmath]x[/ilmath] a bound variable

Additionally:

  • Formulas defined by just [ilmath]\mathrm{F}_1[/ilmath] and [ilmath]\mathrm{F}_2[/ilmath] are called atomic formulas; the rest are composite formulas[2].

[ilmath]\mathscr{L}_\mathrm{F} [/ilmath] denotes the set of formulas of a FOL [ilmath]\mathscr{L} [/ilmath].

Crap is now possible; like [ilmath](x\doteq y)\wedge(x\not\doteq y)[/ilmath], however there are 2 kinds of crap, the first is that which is always crap, like the example I just gave, and some things which are crap given a certain set of assumptions

Notes

  1. ↑ This is done so the author can unambiguously use [ilmath]=[/ilmath] in the "symbols" sense (these are the same) and [ilmath]=[/ilmath] in the sense of "in the FOL we can show these are equal".

References

  1. ↑ 1.0 1.1 1.2 Books:A Course on Mathematical Logic - Shashi Mohan Srivastava
  2. ↑ 2.00 2.01 2.02 2.03 2.04 2.05 2.06 2.07 2.08 2.09 2.10 2.11 2.12 Books:Mathematical Logic - Foundations for Information Science - Wei Li
  3. ↑ 3.0 3.1 3.2 3.3 3.4 3.5 3.6 Books:A Course on Mathematical Logic - Shashi Mohan Srivastava and Books:Mathematical Logic - Foundations for Information Science - Wei Li

OLD PAGE

All from Books:A Course on Mathematical Logic - Shashi Mohan Srivastava

Definition

A first order language, [ilmath]L[/ilmath], consists of two types of symbols:

  1. Logical symbols
    • A sequence of variables, [ilmath]x_1,x_2,\ldots[/ilmath] (this is the alphabetical order of the variables)
    • logical connectives, [ilmath]\neg[/ilmath] (negation), [ilmath]\vee[/ilmath] (disjunction - posh way of saying "or"),
    • a logical quantifier [ilmath]\exists[/ilmath] (existential qualifier) and
    • the equality symbol, [ilmath]=[/ilmath]
  2. Non-logical symbols (which vary from theory to theory)
    • A set of constant symbols, [ilmath]\{c_i\vert i\in I\} [/ilmath],
    • for each positive integer, [ilmath]n\in\mathbb{N}_{\ge 1} [/ilmath] a set of [ilmath]n[/ilmath]-ary function symbols, [ilmath]\{f_j\vert j\in J_n\} [/ilmath]
    • for each positive integer, [ilmath]n\in\mathbb{N}_{\ge 1} [/ilmath] a set of [ilmath]n[/ilmath]-ary relation symbols, [ilmath]\{p_k\vert k\in K_n\} [/ilmath]

Terminology

  • Expression - any finite sequence of symbols of a language.
Retrieved from "http://www.maths.kisogo.com/index.php?title=Notes:First_order_language&oldid=2947"