المرجع الالكتروني للمعلوماتية
المرجع الألكتروني للمعلوماتية

الرياضيات
عدد المواضيع في هذا القسم 9761 موضوعاً
تاريخ الرياضيات
الرياضيات المتقطعة
الجبر
الهندسة
المعادلات التفاضلية و التكاملية
التحليل
علماء الرياضيات

Untitled Document
أبحث عن شيء أخر المرجع الالكتروني للمعلوماتية
أنـواع اتـجاهـات المـستهـلك
2024-11-28
المحرر العلمي
2024-11-28
المحرر في الصحافة المتخصصة
2024-11-28
مـراحل تكويـن اتجاهات المـستهـلك
2024-11-28
عوامـل تكويـن اتـجاهات المـستهـلك
2024-11-28
وسـائـل قـيـاس اتـجاهـات المستهلـك
2024-11-28

Borwein Conjectures
21-8-2019
تفسير الاية (71-73) من سورة يونس
25-3-2020
مميزات الصحافة الإلكترونية
20-12-2020
أهمية الخبرة أمام القضاء
1-8-2017
التسويق المباشر عبر الإذاعة
8/9/2022
Centered Polygonal Number
16-12-2020

First-Order Logic  
  
799   11:39 صباحاً   date: 24-1-2022
Author : Chang, C.-L. and Lee, R. C.-T.
Book or Source : Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.
Page and Part : ...


Read More
Date: 23-1-2022 803
Date: 23-1-2022 536
Date: 9-2-2022 735

First-Order Logic

 

The set of terms of first-order logic (also known as first-order predicate calculus) is defined by the following rules:

1. A variable is a term.

2. If f is an n-place function symbol (with n>=0) and t_1, ..., t_n are terms, then f(t_1,...,t_n) is a term.

If P is an n-place predicate symbol (again with n>=0) and t_1, ..., t_n are terms, then P(t_1,...,t_n) is an atomic statement.

Consider the sentential formulas  forall xB and  exists xB, where B is a sentential formula,  forall  is the universal quantifier ("for all"), and  exists  is the existential quantifier ("there exists"). B is called the scope of the respective quantifier, and any occurrence of variable x in the scope of a quantifier is bound by the closest  forall x or  exists x. The variable x is free in the formula B if at least one of its occurrences in B is not bound by any quantifier within B.

The set of sentential formulas of first-order predicate calculus is defined by the following rules:

1. Any atomic statement is a sentential formula.

2. If B and C are sentential formulas, then ¬B (NOT B), B ^ C (B AND C), B v C (B OR C), and B=>C (B implies C) are sentential formulas (cf. propositional calculus).

3. If B is a sentential formula in which x is a free variable, then  forall xB and  exists xB are sentential formulas.

In formulas of first-order predicate calculus, all variables are object variables serving as arguments of functions and predicates. (In second-order predicate calculus, variables may denote predicates, and quantifiers may apply to variables standing for predicates.) The set of axiom schemata of first-order predicate calculus is comprised of the axiom schemata of propositional calculus together with the two following axiom schemata:

 forall xF(x)=>F(r)

(1)

F(r)=> exists xF(x),

(2)

where F(x) is any sentential formula in which x occurs free, r is a term, F(r) is the result of substituting r for the free occurrences of x in sentential formula F, and all occurrences of all variables in r are free in F.

Rules of inference in first-order predicate calculus are the Modus Ponens and the two following rules:

(G=>F(x))/(G=> forall xF(x))

(3)

(F(x)=>G)/( exists xF(x)=>G),

(4)

where F(x) is any sentential formula in which x occurs as a free variable, x does not occur as a free variable in formula G, and the notation means that if the formula above the line is a theorem formally deducted from axioms by application of inference rules, then the sentential formula below the line is also a formal theorem.

Similarly to propositional calculus, rules for introduction and elimination of  forall  and  exists  can be derived in first-order predicate calculus. For example, the following rule holds provided that F(r) is the result of substituting variable r for the free occurrences of x in sentential formula F and all occurrences of r resulting from this substitution are free in F,

 ( forall xF(x))/(F(r)).

(5)

Gödel's completeness theorem established equivalence between valid formulas of first-order predicate calculus and formal theorems of first-order predicate calculus. In contrast to propositional calculus, use of truth tables does not work for finding valid sentential formulas in first-order predicate calculus because its truth tables are infinite. However, Gödel's completeness theorem opens a way to determine validity, namely by proof.


REFERENCES

Chang, C.-L. and Lee, R. C.-T. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.

Kleene, S. C. Mathematical Logic. New York: Dover, 2002.Mendelson, E. Introduction to Mathematical Logic, 4th ed. London: Chapman & Hall, p. 12, 1997.




الجبر أحد الفروع الرئيسية في الرياضيات، حيث إن التمكن من الرياضيات يعتمد على الفهم السليم للجبر. ويستخدم المهندسون والعلماء الجبر يومياً، وتعول المشاريع التجارية والصناعية على الجبر لحل الكثير من المعضلات التي تتعرض لها. ونظراً لأهمية الجبر في الحياة العصرية فإنه يدرّس في المدارس والجامعات في جميع أنحاء العالم. ويُعجب الكثير من الدارسين للجبر بقدرته وفائدته الكبيرتين، إذ باستخدام الجبر يمكن للمرء أن يحل كثيرًا من المسائل التي يتعذر حلها باستخدام الحساب فقط.وجاء اسمه من كتاب عالم الرياضيات والفلك والرحالة محمد بن موسى الخورازمي.


يعتبر علم المثلثات Trigonometry علماً عربياً ، فرياضيو العرب فضلوا علم المثلثات عن علم الفلك كأنهما علمين متداخلين ، ونظموه تنظيماً فيه لكثير من الدقة ، وقد كان اليونان يستعملون وتر CORDE ضعف القوسي قياس الزوايا ، فاستعاض رياضيو العرب عن الوتر بالجيب SINUS فأنت هذه الاستعاضة إلى تسهيل كثير من الاعمال الرياضية.

تعتبر المعادلات التفاضلية خير وسيلة لوصف معظم المـسائل الهندسـية والرياضـية والعلمية على حد سواء، إذ يتضح ذلك جليا في وصف عمليات انتقال الحرارة، جريان الموائـع، الحركة الموجية، الدوائر الإلكترونية فضلاً عن استخدامها في مسائل الهياكل الإنشائية والوصف الرياضي للتفاعلات الكيميائية.
ففي في الرياضيات, يطلق اسم المعادلات التفاضلية على المعادلات التي تحوي مشتقات و تفاضلات لبعض الدوال الرياضية و تظهر فيها بشكل متغيرات المعادلة . و يكون الهدف من حل هذه المعادلات هو إيجاد هذه الدوال الرياضية التي تحقق مشتقات هذه المعادلات.