Main Page: Difference between revisions

From formulasearchengine
Jump to navigation Jump to search
← Older editNewer edit →
No edit summary
No edit summary
Line 1: Line 1:
In [[chemical thermodynamics]], '''activity''' (symbol ''a'') is a measure of the “effective concentration” of a [[chemical species|species]] in a mixture, meaning that the species' [[chemical potential]] depends on the activity of a real solution in the same way that it would depend on concentration for an [[ideal solution]].  
'''Proof theory''' is a branch of [[mathematical logic]] that represents [[Mathematical proof|proof]]s as formal [[mathematical object]]s, facilitating their analysis by mathematical techniques.  Proofs are typically presented as inductively-defined [[data structures]] such as plain lists, boxed lists, or trees, which are constructed according to the [[axiom]]s and [[rule of inference|rules of inference]] of the logical system.  As such, proof theory is [[syntax (logic)|syntactic]] in nature, in contrast to [[model theory]], which is [[Formal semantics (logic)|semantic]] in nature.  Together with [[model theory]], [[axiomatic set theory]], and [[recursion theory]], proof theory is one of the so-called ''four pillars'' of the [[foundations of mathematics]].<ref name=wang>E.g., Wang (1981), pp. 3–4, and Barwise (1978).</ref>


By convention, activity is treated as a [[dimensionless quantity]], although its actual value depends on customary choices of [[standard state]] for the species. The activity of pure substances in condensed phases (solid or liquids) is normally taken as [[Unity (mathematics)|unity]] (the number 1). Activity depends on temperature, pressure and composition of the mixture, among other things. For gases, the effective partial pressure is usually referred to as [[fugacity]].
Proof theory is important in [[philosophical logic]], where the primary interest is in the idea of a [[proof-theoretic semantics]], an idea which depends upon technical ideas in [[structural proof theory]] to be feasible.


The difference between activity and other measures of composition arises because [[molecule]]s in non-ideal [[gas]]es or [[solution]]s interact with each other, either to attract or to repel each other. The activity of an [[ion]] is particularly influenced by its surroundings.
==History==
Although the formalisation of logic was much advanced by the work of such figures as [[Gottlob Frege]], [[Giuseppe Peano]], [[Bertrand Russell]], and [[Richard Dedekind]], the story of modern proof theory is often seen as being established by [[David Hilbert]], who initiated what is called [[Hilbert's program]] in the [[foundations of mathematics]].  [[Kurt Gödel]]'s seminal work on proof theory first advanced, then refuted this program: his [[Gödel's completeness theorem|completeness theorem]] initially seemed to bode well for Hilbert's aim of reducing all mathematics to a finitist formal system; then his [[Gödel's incompleteness theorem|incompleteness theorems]] showed that this is unattainable. All of this work was carried out with the proof calculi called the [[Hilbert system]]s.


Activities ''should'' be used to define [[equilibrium constant]]s but, in practice, [[concentration]]s are often used instead. The same is often true of equations for [[reaction rate]]s. However, there are circumstances where the activity and the concentration are ''significantly different'' and, as such, it is not valid to approximate with concentrations where activities are required. Two examples serve to illustrate this point:
In parallel, the foundations of [[structural proof theory]] were being founded.  [[Jan Łukasiewicz]] suggested in 1926 that one could improve on [[Hilbert system]]s as a basis for the axiomatic presentation of logic if one  allowed the drawing of conclusions from assumptions in the inference rules of the logic. In response to this [[Stanisław Jaśkowski]] (1929) and [[Gerhard Gentzen]] (1934) independently provided such systems, called calculi of [[natural deduction]], with Gentzen's approach introducing the idea of symmetry between the grounds for asserting propositions, expressed in [[introduction rule]]s, and the consequences of accepting propositions in the [[elimination rule]]s, an idea that has proved very important in proof theory.<ref>{{harvtxt|Prawitz|2006|p=98}}.</ref>  Gentzen (1934) further introduced the idea of the [[sequent calculus]], a calculus advanced in a similar spirit that better expressed the duality of the logical connectives,<ref>Girard, Lafont, and Taylor (1988).</ref> and went on to make fundamental advances in the formalisation of intuitionistic logic,  and provide the first [[combinatorial proof]] of the consistency of [[Peano arithmetic]]. Together, the presentation of natural deduction and the sequent calculus introduced the fundamental idea of [[analytic proof]] to proof theory.
*In a solution of [[potassium hydrogen iodate]] at 0.02&nbsp;[[molar concentration|M]] the activity is 40% lower than the calculated hydrogen ion concentration, resulting in a much higher [[pH]] than expected.
*When a 0.1&nbsp;M [[hydrochloric acid]] solution containing [[methyl green]] [[pH indicator|indicator]] is added to a 5&nbsp;M solution of [[magnesium chloride]], the color of the indicator changes from green to yellow—indicating increasing acidity—when in fact the acid has been diluted. Although at low ionic strength (<0.1&nbsp;M) the [[activity coefficient]] approaches unity, this coefficient can actually increase with ionic strength in a high ionic strength regime. For hydrochloric acid solutions, the minimum is around 0.4&nbsp;M.<ref name="McCarty2006">{{citation | title = pH Paradoxes: Demonstrating that it is not true that pH ≡ -log[H+] | first1 = Christopher G. | last1 = McCarty | first2 = Ed | last2 = Vitz | journal = [[Journal of Chemical Education|J. Chem. Ed.]] | volume = 83 | pages = 752 | year = 2006 | doi = 10.1021/ed083p752 | issue = 5|bibcode = 2006JChEd..83..752M }}</ref>


==Definition==
==Formal and informal proof==<!-- This section is linked from [[Black–Scholes]] and [[Mathematical proof]]-->
The activity of a species ''i'', denoted ''a<sub>i</sub>'', is defined<ref name="GoldBook">{{GoldBookRef|title=activity (relative activity), ''a''|file=A00115}}</ref><ref name="GreenBook">{{GreenBookRef2nd|pages=49–50}}</ref> as:
:<math>a_i = \exp\left (\frac{\mu_i - \mu^{\ominus}_i}{RT}\right )</math>
where ''μ<sub>i</sub>'' is the [[chemical potential]] of the species under the conditions of interest, ''μ''<sup><s>o</s></sup><sub>''i''</sub> is the chemical potential of that species in the chosen [[standard state]], ''R'' is the [[gas constant]] and ''T'' is the [[thermodynamic temperature]]. This definition can also be written in terms of the chemical potential:
:<math>\mu_i = \mu_i^{\ominus} + RT\ln{a_i}</math>
Hence the activity will depend on ''any factor'' that alters the chemical potential. These include temperature, pressure, chemical environment etc. In specialised cases, other factors may have to be considered, such as the presence of an electric or magnetic field or the position in a gravitational field. However, the most common use of activity is to describe the variation in chemical potential with the composition of a mixture.


The activity also depends on the choice of standard state, as it describes the difference between an actual chemical potential and a standard chemical potential. In principle, the choice of standard state is arbitrary, although there are certain conventional standard states which are usually used in different situations.
{{Main|Formal proof}}


===Activity coefficient===
The ''informal'' proofs of everyday mathematical practice are unlike the ''formal'' proofs of proof theory. They are rather like high-level sketches that would allow an expert to reconstruct a formal proof at least in principle, given enough time and patience. For most mathematicians, writing a fully formal proof is too pedantic and long-winded to be in common use.
{{Main|Activity coefficient}}
The activity coefficient ''γ'', which is also a dimensionless quantity, relates the activity to a measured [[amount fraction]] ''x<sub>i</sub>'', [[molality]] ''b<sub>i</sub>'' or [[amount concentration]] ''c<sub>i</sub>'':
:<math>a_{x,i} = \gamma_{x,i} x_i\,</math>
:<math>a_{b,i} = \gamma_{b,i} b_i/b^{\ominus}\,</math> 
:<math>a_{c,i} = \gamma_{c,i} c_i/c^{\ominus}\,</math>
The division by the standard molality ''b''<sup><s>o</s></sup> or the standard amount concentration ''c''<sup><s>o</s></sup> is necessary to ensure that both the activity and the activity coefficient are dimensionless, as is conventional.<ref name="GreenBook"/>


When the activity coefficient is close to one, the substance shows almost ideal behaviour according to [[Henry's law]]. In these cases, the activity can be substituted with the appropriate dimensionless measure of composition ''x<sub>i</sub>'', ''m<sub>i</sub>''/''m''<sup><s>o</s></sup> or ''c<sub>i</sub>''/''c''<sup><s>o</s></sup>. It is also possible to define an activity coefficient in terms of [[Raoult's law]]: the [[International Union of Pure and Applied Chemistry]] (IUPAC) recommends the symbol ƒ for this activity coefficient,<ref name="GreenBook"/> although this should not be confused with [[fugacity]].
Formal proofs are constructed with the help of computers in [[interactive theorem proving]].  
:<math>a_{x,i} = f_i x_i\,</math>. Solution can also become too diluted when necessary.
Significantly, these proofs can be checked automatically, also by computer. (Checking formal proofs is usually simple, whereas ''finding'' proofs ([[automated theorem proving]]) is generally hard.) An informal proof in the mathematics literature, by contrast, requires weeks of [[peer review]] to be checked, and may still contain errors.


==Standard states==
==Kinds of proof calculi==
{{seealso|Standard state}}


===Gases===
The three most well-known styles of [[proof calculi]] are:
In most laboratory situations, the difference in behaviour between a real gas and an ideal gas is dependent only on the pressure and the temperature, not on the presence of any other gases. At a given temperature, the "effective" pressure of a gas  ''i'' is given by its [[fugacity]] ƒ<sub>''i''</sub>: this may be higher or lower than its mechanical pressure. By historical convention, fugacities have the dimension of pressure, so the dimensionless activity is given by:
*The [[Hilbert system|Hilbert calculi]]
:<math>a_i = \frac{f_i}{p^{\ominus}} = \phi_i x_i \frac{p}{p^{\ominus}}</math>
*The [[natural deduction calculus|natural deduction calculi]]
where ''Φ''<sub>''i''</sub> is the dimensionless fugacity coefficient of the species, ''x<sub>i</sub>'' is its fraction in the gaseous mixture (''x''&nbsp;= 1 for a pure gas) and ''p'' is the total pressure. The value ''p''<sup><s>o</s></sup> is the standard pressure: it may be equal to 1&nbsp;atm (101.325&nbsp;kPa) or 1&nbsp;bar (100&nbsp;kPa) depending on the source of data, and should always be quoted.
*The [[sequent calculus|sequent calculi]]


===Mixtures in general===
Each of these can give a complete and axiomatic formalization of [[propositional logic|propositional]] or [[predicate logic]] of either the [[classical logic|classical]] or [[intuitionistic logic|intuitionistic]] flavour, almost any [[modal logic]], and many [[substructural logic]]s, such as [[relevance logic]] or
The most convenient way of expressing the composition of a generic mixture is by using the amount fractions ''x'' of the different components, where
[[linear logic]].  Indeed it is unusual to find a logic that resists being represented in one of these calculi.
:<math>x_i = \frac{n_i}{n}</math>
:<math>\sum_i x_i = 1\,</math>
The standard state of each component in the mixture is taken to be the pure substance, i.e. the pure substance has an activity of one. When activity coefficients are used, they are usually defined in terms of [[Raoult's law]],
:<math>a_i = f_i x_i\,</math>
where ƒ<sub>''i''</sub> is the Raoult's law activity coefficient: an activity coefficient of one indicates ideal behaviour according to Raoult's law.


===Dilute solutions (non-ionic)===
==Consistency proofs==
A solute in dilute solution usually follows [[Henry's law]] rather than Raoult's law, and it is more usual to express the composition of the solution in terms of the amount concentration ''c'' (in mol/L) or  the molality ''b'' (in mol/kg) of the solute rather than in amount fractions. The standard state of a dilute solution is a hypothetical solution of concentration ''c''<sup><s>o</s></sup>&nbsp;= 1&nbsp;mol/L (or molality ''b''<sup><s>o</s></sup>&nbsp;= 1&nbsp;mol/kg) which shows ideal behaviour (also referred to as "infinite-dilution" behaviour). The standard state, and hence the activity, depends on which measure of composition is used. Molalities are often preferred as the volumes of non-ideal mixtures are not strictly additive and are also temperature-dependent: molalities do not depend on volume, whereas amount concentrations do.<ref name="Kaufman2002">{{Citation | first = Myron | last = Kaufman | title = Principles of thermodynamics | page = 213 | publisher = CRC Press | year = 2002 | isbn = 0-8247-0692-7}}</ref>
{{Main|Consistency proof}}


The activity of the solute is given by:
As previously mentioned, the spur for the mathematical investigation of proofs in formal theories was [[Hilbert's program]]. The central idea of this program was that if we could give finitary proofs of consistency for all the sophisticated formal theories needed by mathematicians, then we could ground these theories by means of a metamathematical argument, which shows that all of their purely universal assertions (more technically their provable [[arithmetical hierarchy|<math>\Pi^0_1</math> sentences]]) are finitarily true; once so grounded we do not care about the non-finitary meaning of their existential theorems, regarding these as pseudo-meaningful stipulations of the existence of ideal entities.
:<math>a_{c,i} = \gamma_{c,i}\, \frac{c_i}{c^{\ominus}}</math>
:<math>a_{b,i} = \gamma_{b,i}\, \frac{b_i}{b^{\ominus}}</math>


===Ionic solutions===
The failure of the program was induced by [[Kurt Gödel]]'s [[Gödel's incompleteness theorems|incompleteness theorems]], which showed that any [[ω-consistent theory]] that is sufficiently strong to express certain simple arithmetic truths, cannot prove its own consistency, which on Gödel's formulation is a <math>\Pi^0_1</math> sentence.
When the solute undergoes ionic dissociation in solution (a salt e.g.), the system becomes decidedly non-ideal and we need to take the dissociation process into consideration. We can define activities for the cations and anions separately (''a''<sub>+</sub> and ''a''<sub>–</sub>).


It should be noted however that in a liquid solution the activity coefficient of a given [[ion]] (e.g. Ca<sup>2+</sup>) isn't measurable because it is experimentally impossible to independently measure the electrochemical potential of an ion in solution.  (We cannot add cations without putting in anions at the same time). Therefore one introduces the notions of
Much investigation has been carried out on this topic since, which has in particular led to:
*Refinement of Gödel's result, particularly [[J. Barkley Rosser]]'s refinement, weakening the above requirement of ω-consistency to simple consistency;
*Axiomatisation of the core of Gödel's result in terms of a modal language, [[provability logic]];
*Transfinite iteration of theories, due to [[Alan Turing]] and [[Solomon Feferman]];
*The recent discovery of [[self-verifying theories]], systems strong enough to talk about themselves, but too weak to carry out the [[diagonal lemma|diagonal argument]] that is the key to Gödel's unprovability argument.


;mean ionic activity
==Structural proof theory==
:''a''<sub>±</sub><sup>''ν''</sup> = ''a''<sub>+</sub><sup>''ν''+</sup>''a''<sub>–</sub><sup>''ν''–</sup>
{{Main|Structural proof theory}}
;mean ionic molality
:''b''<sub>±</sub><sup>''ν''</sup> = ''b''<sub>+</sub><sup>''ν''+</sup>''b''<sub>–</sub><sup>''ν''–</sup>
;mean ionic activity coefficient
:''γ''<sub>±</sub><sup>''ν''</sup> = ''γ''<sub>+</sub><sup>''ν''+</sup>''γ''<sub>–</sub><sup>''ν''–</sup>
where ''ν''&nbsp;= ''ν''<sub>+</sub>&nbsp;+ ''ν''<sub>–</sub> represent the stoichiometric coefficients involved in the ionic dissociation process


Even though ''γ''<sub>+</sub> and ''γ''<sub>–</sub> cannot be determined separately, ''γ''<sub>±</sub> is a measureable quantity that can also be predicted for sufficiently dilute systems using [[Debye–Hückel theory]]. For electrolyte-solutions at higher concentrations, Debye-Hückel theory needs to be extended and replaced, e.g., by a [[Pitzer_equations | Pitzer]] electrolyte solution model (see [[#External_links | external links]] below for examples). For the activity of a strong ionic solute (complete dissociation) we can write:
Structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of [[analytic proof]]. The notion of analytic proof was introduced by Gentzen for the sequent calculus; there the analytic proofs are those that are [[cut-elimination theorem|cut-free]]. His natural deduction calculus also supports a notion of analytic proof, as shown by [[Dag Prawitz]]. The definition is slightly more complex: we say the analytic proofs are the [[Natural deduction#Consistency.2C completeness.2C and normal forms|normal forms]], which are related to the notion of normal form in term rewriting.  More exotic proof calculi such as [[Jean-Yves Girard]]'s [[proof net]]s also support a notion of analytic proof.
:''a''<sub>2</sub> = ''a''<sub>±</sub><sup>''ν''</sup> = ''γ''<sub>±</sub><sup>''ν''</sup>''m''<sub>±</sub><sup>''ν''</sup>


==Measurement==
Structural proof theory is connected to [[type theory]] by means of the [[Curry-Howard correspondence]], which observes a structural analogy between the process of normalisation in the natural deduction calculus and beta reduction in the [[typed lambda calculus]].  This provides the foundation for the [[intuitionistic type theory]] developed by [[Per Martin-Löf]], and is often extended to a three way correspondence, the third leg of which are the [[cartesian closed category|cartesian closed categories]].


The most direct way of measuring an activity of a species is to measure its partial vapor pressure in equilibrium with a number of solutions of different strength. For some solutes this is not practical, say sucrose or salt (NaCl) do not have a measurable vapor pressure at ordinary temperatures. However, in such cases it is possible to measure the vapor pressure of the ''solvent'' instead. Using the [[Gibbs–Duhem relation]] it is possible to translate the change in solvent vapor pressures with concentration into activities for the solute.
==Proof-theoretic semantics==
{{Main|proof-theoretic semantics|logical harmony}}


Another way to determine the activity of a species is through the manipulation of [[colligative properties]], specifically freezing point depression. Using freezing point depression techniques, it is possible to calculate the activity of a weak acid from the relation,
In [[linguistics]], [[type-logical grammar]], [[categorial grammar]] and [[Montague grammar]] apply formalisms based on structural proof theory to give a formal [[natural language semantics]].
:<math>m^{\prime} = m(1 + a)\,</math>
where ''m''' is the total molal equilibrium concentration of solute determined by any colligative property measurement(in this case Δ''T''<sub>fus</sub>, ''b'' is the nominal molality obtained from titration and ''a'' is the activity of the species.


There are also electrochemical methods that allow the determination of activity and its coefficient.
==Tableau systems==
{{Main|Method of analytic tableaux}}


The value of the mean ionic activity coefficient ''γ''<sub>±</sub> of [[ion]]s in solution can also be estimated with the [[Debye–Hückel equation]], the [[Davies equation]] or the [[Pitzer equations]].
Analytic tableaux apply the central idea of analytic proof from structural proof theory to provide decision procedures and semi-decision procedures for a wide range of logics.


==Use==
==Ordinal analysis==
Chemical activities should be used to define [[chemical potential]]s, where the chemical potential depends on the [[temperature]] ''T'', [[pressure]] ''p'' and the activity ''a<sub>i</sub>'' according to the [[formula]]:
{{Main|Ordinal analysis}}
:<math>\mu_i = \mu_i^{\ominus} + RT\ln{a_i}</math>
where ''R'' is the [[gas constant]] and ''µ<sub>i</sub>''<sup><s>o</s></sup> is the value of ''µ<sub>i</sub>'' under standard conditions. Note that the choice of concentration scale affects both the activity and the standard state chemical potential, which is especially important when the reference state is the infinite dilution of a solute in a solvent.


Formulae involving activities can be simplified by considering that:
Ordinal analysis is a powerful technique for providing combinatorial consistency proofs for theories formalising arithmetic and analysis.
* For a chemical solution:
** the [[solvent]] has an activity of unity (only a valid approximation for rather dilute solutions)
** At a low concentration, the activity of a solute can be approximated to the ratio of its concentration over the standard concentration:
:<math>a_i = \frac{c_i}{c^{\ominus}}</math>
Therefore, it is approximately equal to its concentration.


* For a mix of [[gas]] at low pressure, the activity is equal to the ratio of the [[partial pressure]] of the gas over the standard pressure:
==Logics from proof analysis==
: <math>a_i = \frac{p_i}{p^{\ominus}}</math>
{{Main|Substructural logic}}
: Therefore, it is equal to the partial pressure in [[Bar (unit)|bars]] (compared to a standard pressure of 1 bar).


* For a solid body, a uniform, single species solid at one bar has an activity of unity. The same thing holds for a pure liquid.
Several important logics have come from insights into logical structure arising in structural proof theory.
 
The latter follows from any definition based on Raoult's law, because if we let the solute concentration ''x''<sub>1</sub> go to zero, the vapor pressure of the solvent ''p'' will go to ''p''*. Thus its activity ''a''&nbsp;= ''p''/''p''* will go to unity. This means that if during a reaction in dilute solution more solvent is generated (the reaction produces water e.g.) we can typically set its activity to unity.
 
Solid and liquid activities do not depend very strongly on pressure because their molar volumes are typically small. [[Graphite]] at 100&nbsp;bars has an activity of only 1.01 if we choose ''p''<sup><s>o</s></sup>&nbsp;= 1&nbsp;bar as standard state. Only at very high pressures do we need to worry about such changes.Changes can also come as a result of too much dilution of solution.
 
==Example values==
Example values of activity coefficients of [[sodium chloride]] in aqueous solution are given in the table.<ref name="Cohen1988">{{citation | first = Paul | last = Cohen | title = The ASME Handbook on Water Technology for Thermal Systems | publisher = American Society of Mechanical Engineers | year = 1988 | page = 567 | isbn = 0-7918-0300-7}}</ref> In an ideal solution, these values would all be unity. The deviations ''tend'' to become larger with increasing molality and temperature, but with some exceptions.
 
{| cellpadding="10" class="wikitable sortable"
|-
![[Molality]] (mol/kg)
! 25 °C
! 50 °C
! 100 °C
! 200 °C
! 300 °C
! 350 °C
|-
| 0.05
| 0.820
| 0.814
| 0.794
| 0.725
| 0.592
| 0.473
|-
| 0.50
| 0.680
| 0.675
| 0.644
| 0.619
| 0.322
| 0.182
|-
|-
| 2.00
| 0.669
| 0.675
| 0.641
| 0.450
| 0.212
| 0.074
|-
| 5.00
| 0.873
| 0.886
| 0.803
| 0.466
| 0.167
| 0.044
|-
|}


==See also==
==See also==
{{Portal|Chemistry}}
{{Portal|Logic}}
*[[Fugacity]], the equivalent of activity for [[partial pressure]]
*[[Intermediate logic]]
*[[Chemical equilibrium]]
*[[Model theory]]
*[[Electrochemical potential]]
*[[Proof (truth)]]
*[[Excess chemical potential]]
*[[Proof techniques]]
*[[Partial molar property]]
*[[Thermodynamic equilibrium]]


==References==
==Notes==
{{Reflist}}
<references/>


==External links==
== References ==
* [http://phasediagram.dk/chemical_potentials.htm Equivalences among different forms of activity coefficients and chemical potentials]
*J. Avigad, E.H. Reck (2001). [http://www.andrew.cmu.edu/user/avigad/Papers/infinite.pdf “Clarifying the nature of the infinite”: the development of metamathematics and proof theory].  Carnegie-Mellon Technical Report CMU-PHIL-120.
* [http://www.aim.env.uea.ac.uk/aim/aim.php Calculate activity coefficients of common inorganic electrolytes and their mixtures]
*J. Barwise (ed., 1978). Handbook of Mathematical Logic. North-Holland.
* [http://www.aiomfac.caltech.edu AIOMFAC online-model]: calculator for activity coefficients of inorganic ions, water, and organic compounds in aqueous solutions and multicomponent mixtures with organic compounds.
*[[A. S. Troelstra]], H. Schwichtenberg (1996). ''Basic Proof Theory''.  In series ''Cambridge Tracts in Theoretical Computer Science'', Cambridge University Press, ISBN 0-521-77911-1.
*G. Gentzen (1935/1969).  Investigations into logical deduction.  In M. E. Szabo, editor, ''Collected Papers of Gerhard Gentzen''. North-Holland.  Translated by Szabo from "Untersuchungen über das logische Schliessen", Mathematisches Zeitschrift 39: 176-210, 405-431.
* {{Springer |title=Proof theory |id=p/p075430}}
*Luis Moreno & [[Bharath Sriraman]] (2005).''Structural Stability and Dynamic Geometry: Some Ideas on Situated Proof. International Reviews on Mathematical Education. Vol. 37, no.3, pp.&nbsp;130–139'' [http://www.springerlink.com/content/n602313107541846/?p=74ab8879ce75445da488d5744cbc3818&pi=0]
*{{cite book|ref=harv|last1=Prawitz|first1=Dag|author1-link=Dag Prawitz|year=2006|origyear=1965|title=Natural deduction: A proof-theoretical study|publisher=Dover Publications|location=Mineola, New York|isbn=978-0-486-44655-4}}
*J. von Plato (2008). [http://plato.stanford.edu/entries/proof-theory-development/ The Development of Proof Theory].  [[Stanford Encyclopedia of Philosophy]].
*{{cite book |last=Wang |first=Hao |authorlink=Hao Wang (academic) |title=Popular Lectures on Mathematical Logic |publisher=[[Van Nostrand|Van Nostrand Reinhold Company]] |year=1981 |isbn= 0-442-23109-1}}


[[Category:Dimensionless numbers of chemistry]]
{{Mathematical logic}}
[[Category:Physical chemistry]]
[[Category:Thermodynamics]]
[[Category:Thermodynamic properties]]


[[ar:فاعلية كيميائية ]]
[[Category:Proof theory| ]]
[[ca:Activitat d'una dissolució]]
{{DEFAULTSORT:Proof Theory}}
[[cs:Aktivita (chemie)]]
[[Category:Mathematical logic| P]]
[[de:Aktivität (Chemie)]]
[[Category:Metalogic]]
[[es:Actividad (química)]]
[[fr:Activité chimique]]
[[it:Attività (chimica)]]
[[lv:Aktivitāte]]
[[nl:Chemische activiteit]]
[[ja:活量]]
[[pl:Aktywność stężeniowa]]
[[pt:Atividade (química)]]
[[ru:Активность (химия)]]
[[sk:Aktivita (termodynamika)]]
[[fi:Aktiivisuus]]
[[sv:Aktivitet (kemi)]]
[[uk:Активність (хімія)]]
[[zh:活性度]]

Revision as of 12:20, 10 August 2014

Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. As such, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature. Together with model theory, axiomatic set theory, and recursion theory, proof theory is one of the so-called four pillars of the foundations of mathematics.[1]

Proof theory is important in philosophical logic, where the primary interest is in the idea of a proof-theoretic semantics, an idea which depends upon technical ideas in structural proof theory to be feasible.

History

Although the formalisation of logic was much advanced by the work of such figures as Gottlob Frege, Giuseppe Peano, Bertrand Russell, and Richard Dedekind, the story of modern proof theory is often seen as being established by David Hilbert, who initiated what is called Hilbert's program in the foundations of mathematics. Kurt Gödel's seminal work on proof theory first advanced, then refuted this program: his completeness theorem initially seemed to bode well for Hilbert's aim of reducing all mathematics to a finitist formal system; then his incompleteness theorems showed that this is unattainable. All of this work was carried out with the proof calculi called the Hilbert systems.

In parallel, the foundations of structural proof theory were being founded. Jan Łukasiewicz suggested in 1926 that one could improve on Hilbert systems as a basis for the axiomatic presentation of logic if one allowed the drawing of conclusions from assumptions in the inference rules of the logic. In response to this Stanisław Jaśkowski (1929) and Gerhard Gentzen (1934) independently provided such systems, called calculi of natural deduction, with Gentzen's approach introducing the idea of symmetry between the grounds for asserting propositions, expressed in introduction rules, and the consequences of accepting propositions in the elimination rules, an idea that has proved very important in proof theory.[2] Gentzen (1934) further introduced the idea of the sequent calculus, a calculus advanced in a similar spirit that better expressed the duality of the logical connectives,[3] and went on to make fundamental advances in the formalisation of intuitionistic logic, and provide the first combinatorial proof of the consistency of Peano arithmetic. Together, the presentation of natural deduction and the sequent calculus introduced the fundamental idea of analytic proof to proof theory.

Formal and informal proof

Mining Engineer (Excluding Oil ) Truman from Alma, loves to spend time knotting, largest property developers in singapore developers in singapore and stamp collecting. Recently had a family visit to Urnes Stave Church.

The informal proofs of everyday mathematical practice are unlike the formal proofs of proof theory. They are rather like high-level sketches that would allow an expert to reconstruct a formal proof at least in principle, given enough time and patience. For most mathematicians, writing a fully formal proof is too pedantic and long-winded to be in common use.

Formal proofs are constructed with the help of computers in interactive theorem proving. Significantly, these proofs can be checked automatically, also by computer. (Checking formal proofs is usually simple, whereas finding proofs (automated theorem proving) is generally hard.) An informal proof in the mathematics literature, by contrast, requires weeks of peer review to be checked, and may still contain errors.

Kinds of proof calculi

The three most well-known styles of proof calculi are:

Each of these can give a complete and axiomatic formalization of propositional or predicate logic of either the classical or intuitionistic flavour, almost any modal logic, and many substructural logics, such as relevance logic or linear logic. Indeed it is unusual to find a logic that resists being represented in one of these calculi.

Consistency proofs

Mining Engineer (Excluding Oil ) Truman from Alma, loves to spend time knotting, largest property developers in singapore developers in singapore and stamp collecting. Recently had a family visit to Urnes Stave Church.

As previously mentioned, the spur for the mathematical investigation of proofs in formal theories was Hilbert's program. The central idea of this program was that if we could give finitary proofs of consistency for all the sophisticated formal theories needed by mathematicians, then we could ground these theories by means of a metamathematical argument, which shows that all of their purely universal assertions (more technically their provable sentences) are finitarily true; once so grounded we do not care about the non-finitary meaning of their existential theorems, regarding these as pseudo-meaningful stipulations of the existence of ideal entities.

The failure of the program was induced by Kurt Gödel's incompleteness theorems, which showed that any ω-consistent theory that is sufficiently strong to express certain simple arithmetic truths, cannot prove its own consistency, which on Gödel's formulation is a sentence.

Much investigation has been carried out on this topic since, which has in particular led to:

  • Refinement of Gödel's result, particularly J. Barkley Rosser's refinement, weakening the above requirement of ω-consistency to simple consistency;
  • Axiomatisation of the core of Gödel's result in terms of a modal language, provability logic;
  • Transfinite iteration of theories, due to Alan Turing and Solomon Feferman;
  • The recent discovery of self-verifying theories, systems strong enough to talk about themselves, but too weak to carry out the diagonal argument that is the key to Gödel's unprovability argument.

Structural proof theory

Mining Engineer (Excluding Oil ) Truman from Alma, loves to spend time knotting, largest property developers in singapore developers in singapore and stamp collecting. Recently had a family visit to Urnes Stave Church.

Structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof. The notion of analytic proof was introduced by Gentzen for the sequent calculus; there the analytic proofs are those that are cut-free. His natural deduction calculus also supports a notion of analytic proof, as shown by Dag Prawitz. The definition is slightly more complex: we say the analytic proofs are the normal forms, which are related to the notion of normal form in term rewriting. More exotic proof calculi such as Jean-Yves Girard's proof nets also support a notion of analytic proof.

Structural proof theory is connected to type theory by means of the Curry-Howard correspondence, which observes a structural analogy between the process of normalisation in the natural deduction calculus and beta reduction in the typed lambda calculus. This provides the foundation for the intuitionistic type theory developed by Per Martin-Löf, and is often extended to a three way correspondence, the third leg of which are the cartesian closed categories.

Proof-theoretic semantics

Mining Engineer (Excluding Oil ) Truman from Alma, loves to spend time knotting, largest property developers in singapore developers in singapore and stamp collecting. Recently had a family visit to Urnes Stave Church.

In linguistics, type-logical grammar, categorial grammar and Montague grammar apply formalisms based on structural proof theory to give a formal natural language semantics.

Tableau systems

Mining Engineer (Excluding Oil ) Truman from Alma, loves to spend time knotting, largest property developers in singapore developers in singapore and stamp collecting. Recently had a family visit to Urnes Stave Church.

Analytic tableaux apply the central idea of analytic proof from structural proof theory to provide decision procedures and semi-decision procedures for a wide range of logics.

Ordinal analysis

Mining Engineer (Excluding Oil ) Truman from Alma, loves to spend time knotting, largest property developers in singapore developers in singapore and stamp collecting. Recently had a family visit to Urnes Stave Church.

Ordinal analysis is a powerful technique for providing combinatorial consistency proofs for theories formalising arithmetic and analysis.

Logics from proof analysis

Mining Engineer (Excluding Oil ) Truman from Alma, loves to spend time knotting, largest property developers in singapore developers in singapore and stamp collecting. Recently had a family visit to Urnes Stave Church.

Several important logics have come from insights into logical structure arising in structural proof theory.

See also

Sportspersons Hyslop from Nicolet, usually spends time with pastimes for example martial arts, property developers condominium in singapore singapore and hot rods. Maintains a trip site and has lots to write about after touring Gulf of Porto: Calanche of Piana.

Notes

  1. ↑ E.g., Wang (1981), pp. 3–4, and Barwise (1978).
  2. ↑ Template:Harvtxt.
  3. ↑ Girard, Lafont, and Taylor (1988).

References

  • J. Avigad, E.H. Reck (2001). “Clarifying the nature of the infinite”: the development of metamathematics and proof theory. Carnegie-Mellon Technical Report CMU-PHIL-120.
  • J. Barwise (ed., 1978). Handbook of Mathematical Logic. North-Holland.
  • A. S. Troelstra, H. Schwichtenberg (1996). Basic Proof Theory. In series Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, ISBN 0-521-77911-1.
  • G. Gentzen (1935/1969). Investigations into logical deduction. In M. E. Szabo, editor, Collected Papers of Gerhard Gentzen. North-Holland. Translated by Szabo from "Untersuchungen über das logische Schliessen", Mathematisches Zeitschrift 39: 176-210, 405-431.
  • Other Sports Official Kull from Drumheller, has hobbies such as telescopes, property developers in singapore and crocheting. Identified some interesting places having spent 4 months at Saloum Delta.

    my web-site http://himerka.com/
  • Luis Moreno & Bharath Sriraman (2005).Structural Stability and Dynamic Geometry: Some Ideas on Situated Proof. International Reviews on Mathematical Education. Vol. 37, no.3, pp. 130–139 [1]
  • 20 year-old Real Estate Agent Rusty from Saint-Paul, has hobbies and interests which includes monopoly, property developers in singapore and poker. Will soon undertake a contiki trip that may include going to the Lower Valley of the Omo.

    My blog: http://www.primaboinca.com/view_profile.php?userid=5889534
  • J. von Plato (2008). The Development of Proof Theory. Stanford Encyclopedia of Philosophy.
  • 20 year-old Real Estate Agent Rusty from Saint-Paul, has hobbies and interests which includes monopoly, property developers in singapore and poker. Will soon undertake a contiki trip that may include going to the Lower Valley of the Omo.

    My blog: http://www.primaboinca.com/view_profile.php?userid=5889534

Template:Mathematical logic

Retrieved from "https://en.formulasearchengine.com/index.php?title=Main_Page&oldid=38215"