Text in Afrikaans, abstract in Afrikaans and English / Die gebruik van simbole maak wiskunde eenvoudiger en kragtiger, maar ook moeiliker verstaanbaar. Laasgenoemde kan voorkom word as slegs eenvoudige en noodsaaklike simbole gebruik word, met die verduidelikings en motiverings in woorde. Die krag van simbole le veral in die feit dat simbole as substitute vir konsepte kan dien. Omdat die krag van simbole hierin le, skuil daar 'n groot gevaar in die gebruik van simbole. Wanneer simbole los is van sinvolle verstandsvoorstellings, is daar geen krag in simbole nie. Dit is die geval met die huidige benadering in skoolalgebra. Voordat voldoende verstandsvoorstellings opgebou is, word daar op die manipulasie van simbole gekonsentreer. Die algebraiese historiese-kenteoretiese perspektief maak algebra meer betekenisvol vir leerders. Hiervolgens moet die leerlinge die geleentheid gegun word om oplossings in prosavorm te skryf en self hul eie wiskundige simbole vir idees spontaan in te voer. Hulle moet self die voordeel van algebraiese simbole beleef. / The use of symbols in algebra both simplifies and strengthens the subject, but it also increases its level of complexity.This problem can be prevented if only simple and essential symbols are used and if the explanations are fully verbalised. The power of symbols stems from their potential to be used as substitutes for concepts. As this constitutes the crux of mathematical symbolic representation, it also presents a danger in that the symbols may not be comprehended. If symbols are not related to mental representations, the symbols are meaningless. This is the case in the present approach to algebra. Before sufficient mental representations are built, there is a concentration on the manipulation of symbols. The algebraic historical epistemological perspective makes algebra more meaningful for learners. Learners should be granted the opportunities to write their solutions in prose and to develop their own symbols for concepts. / Mathematics Education / M. Sc. (Wiskunde-Onderwys)

We show how the non-monotonic nature of common-sense reasoning can be formalised by circumscription. Various forms of circumscription are discussed. A new form of circumscription, namely naive circumscription, is introduced in order to facilitate the comparison of the various forms. Finally, some issues connected with the automation of circumscriptive reasoning are examined. / Computing / M. Sc. (Computer Science)

Orientador: Walter Alexandre Carnielli / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciências Humanas / Made available in DSpace on 2018-08-25T21:09:00Z (GMT). No. of bitstreams: 1 Almeida_HenriqueAntunes_M.pdf: 1516387 bytes, checksum: 2608439ba585a23431d2aa295b1b8876 (MD5) Previous issue date: 2014 / Resumo: Neste trabalho, abordamos o Teorema de Frege sob uma perspectiva exclusivamente técnica. Primeiramente, propomos uma caracterização geral de linguagens de segunda ordem que sejam adequadas para formalizar quaisquer teorias fregeanas ¿ teorias que resultam da introdução de um ou mais princípios de abstração a um sistema dedutivo de lógica de segunda ordem; fornecemos uma semântica e um sistema dedutivo para essas linguagens e elaboramos alguns resultados metateóricos acerca desse sistema. Em segundo lugar, apresentamos uma exposicão detalhada da prova do Teorema de Frege, enunciado como uma relação entre a Aritmética de Frege e a Aritmética de Dedekind-Peano. Por fim, provamos a equiconsistência entre essas teorias e a Aritmética de Peano de Segunda Ordem / Abstract: In this work, we discuss Frege¿s Theorem under an exclusively technical perspective. First, we propose a general caracterization of second-order languages suitable to formalize all Fregean theories ¿ theories that result from the introduction of one or more abstraction principles to a deductive system of second-order logic; we also furnish a semantics and a deductive system for these languages and establish a few metatheorical results about the system. Second, we present a detailed proof of Frege¿s Theorem, formulated as a relation between Frege¿s Arithmetic and Dedekind-Peano Arithemtic. Finally, we prove the equiconsistency between these theories and Peano Second-Order Arithmetic / Mestrado / Filosofia / Mestre em Filosofia

Orientador: Itala Maria Loffredo D'Ottaviano / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciências Humanas / Made available in DSpace on 2018-08-22T15:04:13Z (GMT). No. of bitstreams: 1 Almeida_EdgarLuisBezerrade_M.pdf: 946200 bytes, checksum: e8e316a3ee7420c8d7f45a751651a436 (MD5) Previous issue date: 2013 / Resumo: Esta Dissertação apresenta uma definição de lógica abstrata e caracteriza alguns sistemas lógicos bastante conhecidos na literatura como casos particulares desta. Em especial, mostramos que a lógica de primeira ordem, lógica de segunda ordem, lógica com o operador Q1 de Mostowski e a lógica infinitária L!1! são casos particulares de lógicas abstratas. Mais que isso, mostramos que tais lógicas são regulares. Na análise de cada uma das lógicas acima citadas, mostramos o comportamento das mesmas com relação às propriedades de Löwenheim-Skolem e compacidade enumerável, resultados estes centrais à teoria de modelos. Nossa análise permite-nos constatar que, dentre os quatro casos apresentados, o único que goza de ambas as propriedades é a lógica de primeira ordem; as demais falham em uma, na outra ou em ambas as propriedades. Mostramos que isso não é mera coincidência, mas sim um resultado profundo, que estabelece fronteiras bem delimitadas à lógica de primeira ordem, conhecido como primeiro teorema de Lindström: se uma lógica é regular, ao menos tão expressiva quanto à lógica de primeira ordem e satisfaz ambas as propriedades citadas, então esta é equivalente a lógica de primeira ordem. Realizamos uma prova cuidadosa do teorema, em que cada ideia e cada estratégia de prova é estabelecida criteriosamente. Com seu trabalho, Lindström inaugurou um novo e profícuo campo de estudo, a teoria abstrata de modelos que estabelece, com relação a diversas combinações de propriedades de sistemas lógicos, uma estratificação entre lógicas. Apresentamos um outro exemplo de tal estratificação através de uma versão modal do teorema de Lindström, versão esta que caracteriza a lógica modal básica como maximal quanto a bissimilaridade e compacidade. Encerramos esta Dissertação com algumas considerações acerca da influência do primeiro teorema de Lindström / Abstract: This thesis presents the definition of abstract logic and features some quite logical systems presented in the literature as particular cases of this. In particular, we show that first-order logic, second-order logic, the logic with Mostowski's operator Q1 and the infinitary logic L!1! are specific systems of abstract logic. Moreover, we show that such logics are regular. In the analysis of each above mentioned logical systems we analyses his performance with regard to the properties of compactness and Löwenheim-Skolem, results that have important role in model theory. Our analysis allows us to conclude that among the four cases, the only one who enjoys both properties is the first-order logic, and all others fail in one, other or both properties. We show that this is not mere coincidence, but rather a deep, well-defined boundaries establishing the first-order logic, known as first Lindström's theorem: a regular logic that is at least as expressive as first-order logic and satisfies both properties mentioned, then this is equivalent to first-order logic. We conducted a thorough proof of the theorem, in which each idea and each proof strategy is carefully established. With his work Lindström inaugurated a new and fruitful field of study, the abstract model theory, which establishes with respect to different combinations of properties of logical systems, stratification between logical. Here is another example of such stratification through one of the theorem of modal version Lindström, which characterizes this version of the logic basic modal such as maximal bissimimulation and compactness. We conclude the thesis with some considerations about the influence of the Lindström's theorem / Mestrado / Filosofia / Mestre em Filosofia

M.Sc. / In this thesis we study some of the propertie of a clas called automatic structures. Automatic structures are structures that can be encoded (in some defined way) into a set of regular languages. This encoding allows one to prove many interesting properties about automatic structures, including decidabilty results.

The specification of enterprise information systems using formal specification languages enables the formal verification of these systems. Reasoning about the properties of a formal specification is a tedious task that can be facilitated much through the use of an automated reasoner. However, set theory is a corner stone of many formal specification languages and poses demanding challenges to automated reasoners. To this end a number of heuristics has been developed to aid the Otter theorem prover in finding short proofs for set-theoretic problems. This dissertation investigates the applicability of these heuristics to next generation theorem provers. / Computing / M.Sc. (Computer Science)

We consider a number of temporal logics, some interval-based and some instant-based, and the choices that have to be made if we need to construct a computational framework for such a logic. We consider the axiomatisation of the accessibility relations of the underlying temporal structures when we are using a modal language as well as the formulation of axioms for distinguishing concepts like actions, events, processes and so on for systems using first-order languages. Finally, we briefly discuss the fields of application of temporal logics and list a number of fields that looks promising for further research. / Computer Science & Information Systems / M.Sc.(Computer Science)

<p>This thesis consists of four papers in domain theory and a summary. The first two papers deal with the problem of defining effectivity for continuous cpos. The third and fourth paper present the new notion of an admissible domain representation, where a domain representation D of a space X is λ-admissible if, in principle, all other λ-based domain representations E of X can be reduced to X via a continuous function from E to D. </p><p>In Paper I we define a cartesian closed category of effective bifinite domains. We also investigate the method of inducing effectivity onto continuous cpos via projection pairs, resulting in a cartesian closed category of projections of effective bifinite domains. </p><p>In Paper II we introduce the notion of an almost algebraic basis for a continuous cpo, showing that there is a natural cartesian closed category of effective consistently complete continuous cpos with almost algebraic bases. We also generalise the notion of a complete set, used in Paper I to define the bifinite domains, and investigate what closure results that can be obtained. </p><p>In Paper III we consider admissible domain representations of topological spaces. We present a characterisation theorem of exactly when a topological space has a λ-admissible and κ-based domain representation. We also show that there is a natural cartesian closed category of countably based and countably admissible domain representations. </p><p>In Paper IV we consider admissible domain representations of convergence spaces, where a convergence space is a set X together with a convergence relation between nets on X and elements of X. We study in particular the new notion of weak κ-convergence spaces, which roughly means that the convergence relation satisfies a generalisation of the Kuratowski limit space axioms to cardinality κ. We show that the category of weak κ-convergence spaces is cartesian closed. We also show that the category of weak κ-convergence spaces that have a dense, λ-admissible, κ-continuous and α-based consistently complete domain representation is cartesian closed when α ≤ λ ≥ κ. As natural corollaries we obtain corresponding results for the associated category of weak convergence spaces.</p>

This thesis consists of four papers in domain theory and a summary. The first two papers deal with the problem of defining effectivity for continuous cpos. The third and fourth paper present the new notion of an admissible domain representation, where a domain representation D of a space X is λ-admissible if, in principle, all other λ-based domain representations E of X can be reduced to X via a continuous function from E to D. In Paper I we define a cartesian closed category of effective bifinite domains. We also investigate the method of inducing effectivity onto continuous cpos via projection pairs, resulting in a cartesian closed category of projections of effective bifinite domains. In Paper II we introduce the notion of an almost algebraic basis for a continuous cpo, showing that there is a natural cartesian closed category of effective consistently complete continuous cpos with almost algebraic bases. We also generalise the notion of a complete set, used in Paper I to define the bifinite domains, and investigate what closure results that can be obtained. In Paper III we consider admissible domain representations of topological spaces. We present a characterisation theorem of exactly when a topological space has a λ-admissible and κ-based domain representation. We also show that there is a natural cartesian closed category of countably based and countably admissible domain representations. In Paper IV we consider admissible domain representations of convergence spaces, where a convergence space is a set X together with a convergence relation between nets on X and elements of X. We study in particular the new notion of weak κ-convergence spaces, which roughly means that the convergence relation satisfies a generalisation of the Kuratowski limit space axioms to cardinality κ. We show that the category of weak κ-convergence spaces is cartesian closed. We also show that the category of weak κ-convergence spaces that have a dense, λ-admissible, κ-continuous and α-based consistently complete domain representation is cartesian closed when α ≤ λ ≥ κ. As natural corollaries we obtain corresponding results for the associated category of weak convergence spaces.

The specification of enterprise information systems using formal specification languages enables the formal verification of these systems. Reasoning about the properties of a formal specification is a tedious task that can be facilitated much through the use of an automated reasoner. However, set theory is a corner stone of many formal specification languages and poses demanding challenges to automated reasoners. To this end a number of heuristics has been developed to aid the Otter theorem prover in finding short proofs for set-theoretic problems. This dissertation investigates the applicability of these heuristics to next generation theorem provers. / Computing / M.Sc. (Computer Science)